diff -r 2b6e73df4e5d -r d3a3cc2f0382 src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Wed Aug 18 11:35:24 2021 +0200
+++ b/src/Tools/isac/Knowledge/Rational.thy	Wed Aug 18 16:03:08 2021 +0200
@@ -89,7 +89,7 @@
 
 (*real_times_divide1_eq .. Isa02*) 
   real_times_divide_1_eq:  "-1 * (c / d) = -1 * c / d " and
-  real_times_divide_num:   "a is_const ==> a * (c / d) = a * c / d " and
+  real_times_divide_num:   "a is_num ==> a * (c / d) = a * c / d " and
 
   real_mult_div_cancel2:   "k ~= 0 ==> m * k / (n * k) = m / n" and
 (*real_mult_div_cancel1:   "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
@@ -100,21 +100,21 @@
 			  
   rat_power:               "(a / b) \<up> n = (a \<up> n) / (b \<up> n)" and
 
-  rat_add:         "[| a is_const; b is_const; c is_const; d is_const |] ==> 
+  rat_add:         "[| a is_num; b is_num; c is_num; d is_num |] ==> 
 	           a / c + b / d = (a * d + b * c) / (c * d)" and
-  rat_add_assoc:   "[| a is_const; b is_const; c is_const; d is_const |] ==> 
+  rat_add_assoc:   "[| a is_num; b is_num; c is_num; d is_num |] ==> 
 	           a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and
-  rat_add1:        "[| a is_const; b is_const; c is_const |] ==> 
+  rat_add1:        "[| a is_num; b is_num; c is_num |] ==> 
 	           a / c + b / c = (a + b) / c" and
-  rat_add1_assoc:   "[| a is_const; b is_const; c is_const |] ==> 
+  rat_add1_assoc:   "[| a is_num; b is_num; c is_num |] ==> 
 	           a / c + (b / c + e) = (a + b) / c + e" and
-  rat_add2:        "[| a is_const; b is_const; c is_const |] ==> 
+  rat_add2:        "[| a is_num; b is_num; c is_num |] ==> 
 	           a / c + b = (a + b * c) / c" and
-  rat_add2_assoc:  "[| a is_const; b is_const; c is_const |] ==> 
+  rat_add2_assoc:  "[| a is_num; b is_num; c is_num |] ==> 
 	           a / c + (b + e) = (a + b * c) / c + e" and
-  rat_add3:        "[| a is_const; b is_const; c is_const |] ==> 
+  rat_add3:        "[| a is_num; b is_num; c is_num |] ==> 
 	           a + b / c = (a * c + b) / c" and
-  rat_add3_assoc:   "[| a is_const; b is_const; c is_const |] ==> 
+  rat_add3_assoc:   "[| a is_num; b is_num; c is_num |] ==> 
 	           a + (b / c + e) = (a * c + b) / c + e"
 
 section \<open>Cancellation and addition of fractions\<close>
@@ -414,7 +414,9 @@
       rules = [
         \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
         \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
-        \<^rule_eval>\<open>is_const\<close> (Prog_Expr.eval_const "#is_const_"),
+(*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* )
+        \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
+( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
         \<^rule_thm>\<open>not_true\<close>,
         \<^rule_thm>\<open>not_false\<close>], 
       scr = Rule.Empty_Prog});
@@ -432,10 +434,10 @@
 
         \<^rule_thm_sym>\<open>minus_divide_left\<close>, (*SYM - ?x / ?y = - (?x / ?y)  may come from subst*)
         \<^rule_thm>\<open>rat_add\<close>,
-          (*"[| a is_const; b is_const; c is_const; d is_const |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
-        \<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
-        \<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
-        \<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c" *)
+          (*"[| a is_num; b is_num; c is_num; d is_num |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
+        \<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a / c + b / c = (a + b) / c"*)
+        \<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_num; ?b is_num; ?c is_num |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
+        \<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a + b / c = (a * c) / c + b / c" *)
         
         \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*)
         \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*)
@@ -626,6 +628,7 @@
         \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
       scr = Rule.Empty_Prog});
 
+\<close> ML \<open>
 (*.contains absolute minimum of thms for context in norm_Rational.*)
 val rat_mult_divide = prep_rls'(
   Rule_Def.Repeat {id = "rat_mult_divide", preconds = [], 
@@ -643,6 +646,7 @@
 	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
       scr = Rule.Empty_Prog});
 
+\<close> ML \<open>
 (*.contains absolute minimum of thms for context in norm_Rational.*)
 val reduce_0_1_2 = prep_rls'(
   Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
@@ -664,15 +668,23 @@
       \<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)],
     scr = Rule.Empty_Prog});
 
+\<close> ML \<open>
+\<close> ML \<open>@{term "1 is_num"}\<close> (*.."Prog_Expr.is_num" IS KNOWN TOODOO*)
+ML \<open>
 (*erls for calculate_Rational; 
   make local with FIXX@ME result:term *term list WN0609???SKMG*)
 val norm_rat_erls = prep_rls'(
   Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
     rules = [
-      \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")],
+      \<^rule_thm>\<open>refl\<close> (* ..DELETE, just to avoid ERROR fun #> not applicable to "[]"*)
+(*/----- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly -------\* )
+      \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")
+( *\---- TOODOO from 2b6e73df4e5d assoc_calc: 'Prog_Expr.is_num' not found in theory Poly ------/*)
+],
     scr = Rule.Empty_Prog});
 
+\<close> ML \<open>
 (* consists of rls containing the absolute minimum of thms *)
 (*
   which is now replaced by MGs version "norm_Rational" below
@@ -693,6 +705,7 @@
 	     ],
     scr = Rule.Empty_Prog});
 
+\<close> ML \<open>
 val norm_Rational_parenthesized = prep_rls'(
   Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list, 
     rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),