1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Apr 15 11:11:54 2020 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Wed Apr 15 11:37:43 2020 +0200
     1.3 @@ -346,7 +346,7 @@
     1.4  	       (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ = 
     1.5      (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
     1.6  	 (SOME n1', SOME n2') =>
     1.7 -  if Num_Calc.calc_equ (strip_thy op0) (n1', n2')
     1.8 +  if Eval.calc_equ (strip_thy op0) (n1', n2')
     1.9      then SOME (TermC.mk_thmid thmid n1 n2, 
    1.10  	  HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.11    else SOME (TermC.mk_thmid thmid n1 n2,  
    1.12 @@ -364,7 +364,7 @@
    1.13  
    1.14  > val t = str2term "1 = 0";
    1.15  > val NONE = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
    1.16 ------------ thus needs Rule.Num_Calc !
    1.17 +----------- thus needs Rule.Eval !
    1.18  > val t = str2term "0 = 0";
    1.19  > val SOME (t',_) = rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false reflI t;
    1.20  > UnparseC.term t';
    1.21 @@ -440,9 +440,9 @@
    1.22      (case (ThmC_Def.int_opt_of_string n1, ThmC_Def.int_opt_of_string n2) of
    1.23      	(SOME n1', SOME n2') =>
    1.24          let 
    1.25 -          val sg = Num_Calc.sign_mult n1' n2';
    1.26 +          val sg = Eval.sign_mult n1' n2';
    1.27            val (T1,T2,Trange) = TermC.dest_binop_typ t0;
    1.28 -          val gcd' = Num_Calc.gcd (abs n1') (abs n2');
    1.29 +          val gcd' = Eval.gcd (abs n1') (abs n2');
    1.30          in if gcd' = abs n2' 
    1.31             then let val rhs = TermC.term_of_num Trange (sg * (abs n1') div gcd')
    1.32      	        val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, rhs))
    1.33 @@ -533,7 +533,7 @@
    1.34  
    1.35  subsection \<open>extend rule-set for evaluating pre-conditions and program-expressions\<close>
    1.36  ML \<open>
    1.37 -val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
    1.38 +val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
    1.39  \<close> ML \<open>
    1.40  \<close> ML \<open>
    1.41  \<close>