diff -r 19bd2f740479 -r 03e19793d81e src/Tools/isac/Knowledge/Base_Tools.thy
--- a/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Aug 04 15:38:42 2022 +0200
+++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Thu Aug 04 16:48:37 2022 +0200
@@ -24,7 +24,7 @@
 
 
 subsection \<open>setup for ML-functions\<close>
-text \<open>required by "eval_binop" below\<close>
+text \<open>required by "Calc_Binop.numeric" below\<close>
 calculation occurs_in = \<open>Prog_Expr.eval_occurs_in "#occurs_in_"\<close>
 calculation some_occur_in = \<open>Prog_Expr.eval_some_occur_in "#some_occur_in_"\<close>
 calculation is_atom = \<open>Prog_Expr.eval_is_atom "#is_atom_"\<close>
@@ -33,11 +33,11 @@
 calculation leq (less_eq) = \<open>Prog_Expr.eval_equ "#less_equal_"\<close>
 calculation ident = \<open>Prog_Expr.eval_ident "#ident_"\<close>
 calculation equal (HOL.eq) = \<open>Prog_Expr.eval_equal "#equal_"\<close>
-calculation PLUS (plus) = \<open>(**)eval_binop "#add_"\<close>
-calculation MINUS (minus) = \<open>(**)eval_binop "#sub_"\<close>
-calculation TIMES (times) = \<open>(**)eval_binop "#mult_"\<close>
+calculation PLUS (plus) = \<open>(**)Calc_Binop.numeric "#add_"\<close>
+calculation MINUS (minus) = \<open>(**)Calc_Binop.numeric "#sub_"\<close>
+calculation TIMES (times) = \<open>(**)Calc_Binop.numeric "#mult_"\<close>
 calculation DIVIDE (divide) = \<open>Prog_Expr.eval_cancel "#divide_e"\<close>
-calculation POWER (realpow) = \<open>(**)eval_binop "#power_"\<close>
+calculation POWER (realpow) = \<open>(**)Calc_Binop.numeric "#power_"\<close>
 calculation boollist2sum = \<open>Prog_Expr.eval_boollist2sum ""\<close>
 
 subsection \<open>rewrite-order for rule-sets\<close>
@@ -115,11 +115,11 @@
 \<close>
 
 subsection \<open>ONCE AGAIN extend rule-set for evaluating pre-conditions and program-expressions\<close>
-text \<open>requires "eval_binop" from above\<close>
+text \<open>requires "Calc_Binop.numeric" from above\<close>
 ML \<open>
 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr [
-  \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
-	\<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), 
+  \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
+	\<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), 
 	\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
 	\<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
 	\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
@@ -135,7 +135,7 @@
     erls = Rule_Def.Repeat {id = "list_elrs", preconds = [], rew_ord = ("termlessI", termlessI), 
     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
-      \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
+      \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"),
       \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_") (*..for nth_Cons_*)],
     scr = Rule.Empty_Prog},
     srls = Rule_Set.Empty, calc = [], errpatts = [],