1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Mon Apr 06 11:44:36 2020 +0200
1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Apr 08 12:32:51 2020 +0200
1.3 @@ -360,13 +360,13 @@
1.4 > reflI;
1.5 val it = "(?t = ?t) = True"
1.6 > val t = str2term "x = 0";
1.7 -> val NONE = rewrite_ thy Rule.dummy_ord Rule_Set.e_rls false reflI t;
1.8 +> val NONE = rewrite_ thy Rule.dummy_ord Rule_Set.empty false reflI t;
1.9
1.10 > val t = str2term "1 = 0";
1.11 -> val NONE = rewrite_ thy Rule.dummy_ord Rule_Set.e_rls false reflI t;
1.12 +> val NONE = rewrite_ thy Rule.dummy_ord Rule_Set.empty false reflI t;
1.13 ----------- thus needs Rule.Num_Calc !
1.14 > val t = str2term "0 = 0";
1.15 -> val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule_Set.e_rls false reflI t;
1.16 +> val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule_Set.empty false reflI t;
1.17 > Rule.term2str t';
1.18 val it = "HOL.True"
1.19
1.20 @@ -533,7 +533,7 @@
1.21
1.22 subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>
1.23 ML \<open>
1.24 -val prog_expr = Rule_Set.append_rls "prog_expr" prog_expr [Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
1.25 +val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
1.26 \<close> ML \<open>
1.27 \<close> ML \<open>
1.28 \<close>