1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Fri Jan 17 12:37:21 2020 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Fri Jan 17 13:14:11 2020 +0100
     1.3 @@ -44,7 +44,7 @@
     1.4  (** eval functions **)
     1.5  
     1.6  val c = Free ("c", HOLogic.realT);
     1.7 -(*.create a new unique variable 'c..' in a term; for use by Rule.Calc in a rls;
     1.8 +(*.create a new unique variable 'c..' in a term; for use by Rule.Num_Calc in a rls;
     1.9     an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
    1.10     in the script; this will be possible if currying doesnt take the value
    1.11     from a variable, but the value '(new_c es__)' itself.*)
    1.12 @@ -118,7 +118,7 @@
    1.13  		     erls = Rule.Erls, 
    1.14  		     srls = Rule.Erls, calc = [], errpatts = [],
    1.15  		     rules = [(*for rewriting conditions in Thm's*)
    1.16 -			      Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
    1.17 +			      Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
    1.18  			      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    1.19  			      Rule.Thm ("not_false",@{thm not_false})
    1.20  			      ],
    1.21 @@ -130,7 +130,7 @@
    1.22  		  Rule.Thm ("integral_add", TermC.num_str @{thm integral_add}),
    1.23  		  Rule.Thm ("integral_mult", TermC.num_str @{thm integral_mult}),
    1.24  		  Rule.Thm ("integral_pow", TermC.num_str @{thm integral_pow}),
    1.25 -		  Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")(*for n+1*)
    1.26 +		  Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")(*for n+1*)
    1.27  		  ],
    1.28  	 scr = Rule.EmptyScr};
    1.29  \<close>
    1.30 @@ -143,8 +143,8 @@
    1.31  		     rew_ord = ("termlessI",termlessI), 
    1.32  		     erls = Rule.Erls, 
    1.33  		     srls = Rule.Erls, calc = [], errpatts = [],
    1.34 -		     rules = [Rule.Calc ("Prog_Expr.matches", Prog_Expr.eval_matches""),
    1.35 -			      Rule.Calc ("Integrate.is'_f'_x", 
    1.36 +		     rules = [Rule.Num_Calc ("Prog_Expr.matches", Prog_Expr.eval_matches""),
    1.37 +			      Rule.Num_Calc ("Integrate.is'_f'_x", 
    1.38  				    eval_is_f_x "is_f_x_"),
    1.39  			      Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
    1.40  			      Rule.Thm ("not_false", TermC.num_str @{thm not_false})
    1.41 @@ -171,7 +171,7 @@
    1.42  		       rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.43  		       erls = (*FIXME.WN051028 Rule.e_rls,*)
    1.44  		       Rule.append_rls "Rule.e_rls-is_polyexp" Rule.e_rls
    1.45 -				  [Rule.Calc ("Poly.is'_polyexp", 
    1.46 +				  [Rule.Num_Calc ("Poly.is'_polyexp", 
    1.47  					 eval_is_polyexp "")],
    1.48  				  srls = Rule.Erls, calc = [], errpatts = [],
    1.49  				  rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
    1.50 @@ -190,7 +190,7 @@
    1.51  	       Rule.Thm ("divide_divide_eq_left",
    1.52                       TermC.num_str @{thm divide_divide_eq_left}),
    1.53  	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
    1.54 -	       Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.55 +	       Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.56  	      
    1.57  	       Rule.Thm ("rat_power", TermC.num_str @{thm rat_power})
    1.58  		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
    1.59 @@ -254,7 +254,7 @@
    1.60  	       Rule.Rls_ discard_parentheses,
    1.61  	       (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
    1.62  	       Rule.Rls_ separate_bdv2,
    1.63 -	       Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
    1.64 +	       Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
    1.65  	       ],
    1.66        scr = Rule.EmptyScr};      
    1.67  
    1.68 @@ -292,7 +292,7 @@
    1.69  * 				  TermC.num_str @{thm add_divide_distrib})
    1.70  * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
    1.71  * 			  ]),
    1.72 -* 	       Rule.Calc ("Rings.divide_class.divide"  , eval_cancel "#divide_e")
    1.73 +* 	       Rule.Num_Calc ("Rings.divide_class.divide"  , eval_cancel "#divide_e")
    1.74  * 	       ],
    1.75  *       scr = Rule.EmptyScr
    1.76  *       });