1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Apr 01 19:20:05 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Sat Apr 04 12:11:32 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.e_rls false reflI t;
     1.8 +> val NONE = rewrite_ thy Rule.dummy_ord Rule_Set.e_rls false reflI t;
     1.9  
    1.10  > val t = str2term "1 = 0";
    1.11 -> val NONE = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
    1.12 +> val NONE = rewrite_ thy Rule.dummy_ord Rule_Set.e_rls 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.e_rls false reflI t;
    1.16 +> val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule_Set.e_rls 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.append_rls "prog_expr" prog_expr [Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
    1.25 +val prog_expr = Rule_Set.append_rls "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>