1.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Fri Jan 17 12:37:21 2020 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Fri Jan 17 13:14:11 2020 +0100
     1.3 @@ -346,7 +346,7 @@
     1.4  	       (Const (op0, _) $ Free (n1, _) $ Free(n2, _))) _ = 
     1.5      (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
     1.6  	 (SOME n1', SOME n2') =>
     1.7 -  if Calc.calc_equ (strip_thy op0) (n1', n2')
     1.8 +  if Num_Calc.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 Rule.dummy_ord Rule.e_rls false reflI t;
    1.16 ------------ thus needs Rule.Calc !
    1.17 +----------- thus needs Rule.Num_Calc !
    1.18  > val t = str2term "0 = 0";
    1.19  > val SOME (t',_) = rewrite_ thy Rule.dummy_ord Rule.e_rls false reflI t;
    1.20  > Rule.term2str t';
    1.21 @@ -461,9 +461,9 @@
    1.22      (case (TermC.int_of_str_opt n1, TermC.int_of_str_opt n2) of
    1.23      	(SOME n1', SOME n2') =>
    1.24          let 
    1.25 -          val sg = Calc.sign_mult n1' n2';
    1.26 +          val sg = Num_Calc.sign_mult n1' n2';
    1.27            val (T1,T2,Trange) = TermC.dest_binop_typ t0;
    1.28 -          val gcd' = Calc.gcd (abs n1') (abs n2');
    1.29 +          val gcd' = Num_Calc.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 @@ -554,7 +554,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 list_rls = Rule.append_rls "list_rls" list_rls [Rule.Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
    1.38 +val list_rls = Rule.append_rls "list_rls" list_rls [Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs "")];
    1.39  \<close> ML \<open>
    1.40  \<close> ML \<open>
    1.41  \<close>