Commit a3d410ab authored by Heiko Becker's avatar Heiko Becker

Add lexer adn parser to translation and start inspecting preconditions"

parent d2581f0d
......@@ -348,6 +348,8 @@ val validIvbounds_v_thm = translate validIntervalbounds_def;
val res = translate CertificateCheckerCmd_def;
val res' = translate runChecker_def;
val invertinterval_side_def = fetch "-" "invertinterval_side_def";
val divideinterval_side_def = fetch "-" "divideinterval_side_def";
......@@ -362,6 +364,16 @@ val validerrorboundcmd_side_def = fetch "-" "validerrorboundcmd_side_def";
val certificatecheckercmd_side_def = fetch "-" "certificatecheckercmd_side_def";
val parseiv_side_def = fetch "-" "parseiv_side_def";
val parseprecond_side_def = fetch "-" "parseprecondrec_side_def";
val parseprecond_side_def = fetch "-" "parseprecond_side_def";
val parse_side_def = fetch "-" "parse_side_def";
val runchecker_side_def = fetch "-" "runchecker_side_def";
val precond_validIntervalbounds_true = prove (
``!f absenv P (dVars:num_set).
(v. v (domain dVars) valid (FST (absenv (Var v)))) ==>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment