diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Test.thy
--- a/src/Tools/isac/Knowledge/Test.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Test.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -378,9 +378,9 @@
 	     \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
 	     \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
     
-	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
-	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+	     \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
+	     \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+	     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
     
 	     \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
 	     \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
@@ -421,10 +421,10 @@
 	     \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
 	     \<^rule_eval>\<open>contains_root\<close> (eval_contains_root"#contains_root_"),
     
-	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
-	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+	     \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
+	     \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
 	     \<^rule_eval>\<open>sqrt\<close> (eval_sqrt "#sqrt_"),
-	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+	     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
     
 	     \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
 	     \<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
@@ -494,10 +494,10 @@
 	     \<^rule_thm>\<open>radd_real_const\<close>,
 	     (* these 2 rules are invers to distr_div_right wrt. termination.
 		     thus they MUST be done IMMEDIATELY before calc *)
-	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
-	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
+	     \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+	     \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
 	     \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
-	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+	     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
 
 	     \<^rule_thm>\<open>rcollect_right\<close>,
 	     \<^rule_thm>\<open>rcollect_one_left\<close>,
@@ -599,9 +599,9 @@
     rew_ord = ("ord_make_polytest", ord_make_polytest false @{theory "Poly"}),
     erls = testerls, srls = Rule_Set.Empty,
     calc = [
-      ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), 
-	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
-	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
+      ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")), 
+	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
+	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))],
     errpatts = [],
     rules = [
        \<^rule_thm>\<open>real_diff_minus\<close>, (*"a - b = a + (-1) * b"*)
@@ -630,18 +630,18 @@
 	     \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
 	     \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
     
-	     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
-	     \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-	     \<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
+	     \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+	     \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+	     \<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
     scr = Rule.Empty_Prog}; 
 
 val expand_binomtest =
   Rule_Def.Repeat{id = "expand_binomtest", preconds = [], 
     rew_ord = ("termlessI",termlessI), erls = testerls, srls = Rule_Set.Empty,
     calc = [
-      ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")), 
-	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
-	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))
+      ("PLUS"  , (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")), 
+	    ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
+	    ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))
 	    ],
     errpatts = [],
     rules = [
@@ -664,9 +664,9 @@
     	\<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
     	\<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
     
-    	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
-    	\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-    	\<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_"),
+    	\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+    	\<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+    	\<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_"),
     
     	\<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
     	\<^rule_thm>\<open>realpow_plus_1\<close>,	 (*"r * r \<up> n = r \<up> (n + 1)"*)
@@ -678,9 +678,9 @@
     	\<^rule_thm>\<open>real_one_collect\<close>,	 (*"m is_num ==> n + m * n = (1 + m) * n"*)
     	\<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
     
-    	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
-    	\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-    	\<^rule_eval>\<open>realpow\<close> (**)(eval_binop "#power_")],
+    	\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
+    	\<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+    	\<^rule_eval>\<open>realpow\<close> (**)(Calc_Binop.numeric "#power_")],
     scr = Rule.Empty_Prog};      
 \<close>
 rule_set_knowledge