# HG changeset patch
# User wenzelm
# Date 1623514927 -7200
# Node ID 09106b85d3b4bb2e9a4312eaa53340bfc508039a
# Parent  73e7175a7d3f0853707b63012096848706c46368
use more antiquotations;

diff -r 73e7175a7d3f -r 09106b85d3b4 src/Tools/isac/Knowledge/Integrate.thy
--- a/src/Tools/isac/Knowledge/Integrate.thy	Sat Jun 12 18:06:27 2021 +0200
+++ b/src/Tools/isac/Knowledge/Integrate.thy	Sat Jun 12 18:22:07 2021 +0200
@@ -120,7 +120,7 @@
 		     rules = [(*for rewriting conditions in Thm's*)
 			      \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
 			      \<^rule_thm>\<open>not_true\<close>,
-			      Rule.Thm ("not_false",@{thm not_false})
+			      \<^rule_thm>\<open>not_false\<close>
 			      ],
 		     scr = Rule.Empty_Prog}, 
 	 srls = Rule_Set.Empty, calc = [], errpatts = [],
@@ -179,14 +179,11 @@
 	       \<^rule_thm>\<open>rat_mult_poly_r\<close>,
 	       (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
 
-	       Rule.Thm ("real_divide_divide1_mg",
-                     ThmC.numerals_to_Free @{thm real_divide_divide1_mg}),
+	       \<^rule_thm>\<open>real_divide_divide1_mg\<close>,
 	       (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
-	       Rule.Thm ("divide_divide_eq_right", 
-                     ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
+	       \<^rule_thm>\<open>divide_divide_eq_right\<close>,
 	       (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
-	       Rule.Thm ("divide_divide_eq_left",
-                     ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
+	       \<^rule_thm>\<open>divide_divide_eq_left\<close>,
 	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
 	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
 	      
@@ -233,8 +230,7 @@
 		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
 		\<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
 			  (*"?bdv  \<up>  ?n / ?b = 1 / ?b * ?bdv  \<up>  ?n"*)
-			  *****Rule.Thm ("add_divide_distrib", 
-			  ***** ThmC.numerals_to_Free @{thm add_divide_distrib})
+			  *****\<^rule_thm>\<open>add_divide_distrib\<close>
 			  (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
 		];
 val simplify_Integral = 
@@ -286,8 +282,7 @@
 * 			  (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
 * 			  \<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
 * 			  (*"?bdv  \<up>  ?n / ?b = 1 / ?b * ?bdv  \<up>  ?n"*)
-* 			  Rule.Thm ("add_divide_distrib", 
-* 				  ThmC.numerals_to_Free @{thm add_divide_distrib})
+* 			  \<^rule_thm>\<open>add_divide_distrib\<close>
 * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
 * 			  ]),
 * 	       \<^rule_eval>\<open>divide\<close> (eval_cancel "#divide_e")
diff -r 73e7175a7d3f -r 09106b85d3b4 src/Tools/isac/Knowledge/Inverse_Z_Transform.thy
--- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sat Jun 12 18:06:27 2021 +0200
+++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sat Jun 12 18:22:07 2021 +0200
@@ -31,7 +31,7 @@
 	  erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
 	  rules = 
 	   [
-    Rule.Thm ("rule4", @{thm rule4})
+    \<^rule_thm>\<open>rule4\<close>
 	   ], 
 	 scr = Rule.Empty_Prog});
 \<close>
@@ -126,9 +126,9 @@
                     (*2nd NTH_CONS pushes n+-1 into asms*)
                     \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], 
               srls = Rule_Set.Empty, calc = [], errpatts = [],
-              rules = [Rule.Thm ("NTH_CONS", @{thm NTH_CONS}),
+              rules = [\<^rule_thm>\<open>NTH_CONS\<close>,
                   \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
-                  Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
+                  \<^rule_thm>\<open>NTH_NIL\<close>,
                   \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
                   \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs"eval_rhs_"),
                   \<^rule_eval>\<open>Prog_Expr.argument_in\<close> (Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
diff -r 73e7175a7d3f -r 09106b85d3b4 src/Tools/isac/Knowledge/Poly.thy
--- a/src/Tools/isac/Knowledge/Poly.thy	Sat Jun 12 18:06:27 2021 +0200
+++ b/src/Tools/isac/Knowledge/Poly.thy	Sat Jun 12 18:22:07 2021 +0200
@@ -745,11 +745,9 @@
 	 \<^rule_thm>\<open>real_plus_minus_binom2_p_p\<close>,
 	     (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
 	      
-	 Rule.Thm ("real_add_mult_distrib_poly",
-               ThmC.numerals_to_Free @{thm real_add_mult_distrib_poly}),
+	 \<^rule_thm>\<open>real_add_mult_distrib_poly\<close>,
 	       (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
-	 Rule.Thm("real_add_mult_distrib2_poly",
-              ThmC.numerals_to_Free @{thm real_add_mult_distrib2_poly}),
+	 \<^rule_thm>\<open>real_add_mult_distrib2_poly\<close>,
 	     (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
 	       
 	 \<^rule_thm>\<open>realpow_multI_poly\<close>,
@@ -773,12 +771,10 @@
 
 	       \<^rule_thm>\<open>realpow_plus_1\<close>,		
 	       (*"r * r \<up> n = r \<up> (n + 1)"*)
-	       Rule.Thm ("realpow_plus_1_assoc_l",
-                     ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l}),
+	       \<^rule_thm>\<open>realpow_plus_1_assoc_l\<close>,
 	       (*"r * (r \<up> m * s) = r \<up> (1 + m) * s"*)
 	       (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a \<up> 2*(a*b) *)
-	       Rule.Thm ("realpow_plus_1_assoc_l2",
-                     ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l2}),
+	       \<^rule_thm>\<open>realpow_plus_1_assoc_l2\<close>,
 	       (*"r \<up> m * (r * s) = r \<up> (1 + m) * s"*)
 
 	       \<^rule_thm_sym>\<open>realpow_addI\<close>,
@@ -895,11 +891,9 @@
 	       (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
 	       \<^rule_thm>\<open>real_minus_binom_pow2_p\<close>,
 	       (*"(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2"*)
-	       Rule.Thm ("real_plus_minus_binom1_p",
-		    ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p}),
+	       \<^rule_thm>\<open>real_plus_minus_binom1_p\<close>,
 	       (*"(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2"*)
-	       Rule.Thm ("real_plus_minus_binom2_p",
-		    ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p}),
+	       \<^rule_thm>\<open>real_plus_minus_binom2_p\<close>,
 	       (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
 
 	       \<^rule_thm>\<open>minus_minus\<close>,
@@ -909,8 +903,7 @@
 	       \<^rule_thm_sym>\<open>real_mult_minus1\<close>
 	       (*- ?z = "-1 * ?z"*)
 
-	       (*Rule.Thm ("real_minus_add_distrib",
-		      ThmC.numerals_to_Free @{thm real_minus_add_distrib}),*)
+	       (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*)
 	       (*"- (?x + ?y) = - ?x + - ?y"*)
 	       (*\<^rule_thm>\<open>real_diff_plus\<close>*)
 	       (*"a - b = a + -b"*)
@@ -968,11 +961,9 @@
 	       (*"1 * z = z"*)
 	       (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*)
 	       (*"-1 * z = - z"*)
-	       Rule.Thm ("minus_mult_left", 
-		    ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),
+	       Rule.Thm ("minus_mult_left", ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),
 	       (*- (?x * ?y) = "- ?x * ?y"*)
-	       (*Rule.Thm ("real_minus_mult_cancel",
-                       ThmC.numerals_to_Free @{thm real_minus_mult_cancel}),
+	       (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>,
 	       (*"- ?x * - ?y = ?x * ?y"*)---*)
 	       \<^rule_thm>\<open>mult_zero_left\<close>,        
 	       (*"0 * z = 0"*)
@@ -1289,23 +1280,17 @@
 	      ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
 	      ("POWER", ("Transcendental.powr", eval_binop "#power_"))
 	      ], errpatts = [],
-      rules = [Rule.Thm ("real_plus_binom_pow2",
-                     ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),     
+      rules = [\<^rule_thm>\<open>real_plus_binom_pow2\<close>,     
 	       (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
-	       Rule.Thm ("real_plus_binom_times",
-                     ThmC.numerals_to_Free @{thm real_plus_binom_times}),    
+	       \<^rule_thm>\<open>real_plus_binom_times\<close>,    
 	      (*"(a + b)*(a + b) = ...*)
-	       Rule.Thm ("real_minus_binom_pow2",
-                     ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),   
+	       \<^rule_thm>\<open>real_minus_binom_pow2\<close>,   
 	       (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
-	       Rule.Thm ("real_minus_binom_times",
-                     ThmC.numerals_to_Free @{thm real_minus_binom_times}),   
+	       \<^rule_thm>\<open>real_minus_binom_times\<close>,   
 	       (*"(a - b)*(a - b) = ...*)
-	       Rule.Thm ("real_plus_minus_binom1",
-                     ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),   
+	       \<^rule_thm>\<open>real_plus_minus_binom1\<close>,   
 		(*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
-	       Rule.Thm ("real_plus_minus_binom2",
-                     ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),   
+	       \<^rule_thm>\<open>real_plus_minus_binom2\<close>,   
 		(*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
 	       (*RL 020915*)
 	       \<^rule_thm>\<open>real_pp_binom_times\<close>, 
@@ -1320,8 +1305,7 @@
 		(*(a*b) \<up> n = a \<up> n * b \<up> n*)
 	       \<^rule_thm>\<open>real_plus_binom_pow3\<close>,
 	        (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
-	       Rule.Thm ("real_minus_binom_pow3",
-                     ThmC.numerals_to_Free @{thm real_minus_binom_pow3}),
+	       \<^rule_thm>\<open>real_minus_binom_pow3\<close>,
 	        (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
 
 
@@ -1345,8 +1329,7 @@
 	       \<^rule_eval>\<open>powr\<close> (eval_binop "#power_"),
               (*\<^rule_thm>\<open>mult.commute\<close>,
 		(*AC-rewriting*)
-	       Rule.Thm ("real_mult_left_commute",
-                     ThmC.numerals_to_Free @{thm real_mult_left_commute}),
+	       \<^rule_thm>\<open>real_mult_left_commute\<close>,
 	       \<^rule_thm>\<open>mult.assoc\<close>,
 	       \<^rule_thm>\<open>add.commute\<close>,
 	       \<^rule_thm>\<open>add.left_commute\<close>,
@@ -1363,14 +1346,12 @@
 
 	       \<^rule_thm>\<open>real_num_collect\<close>, 
 	       (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
-	       Rule.Thm ("real_num_collect_assoc",
-                     ThmC.numerals_to_Free @{thm real_num_collect_assoc}),	
+	       \<^rule_thm>\<open>real_num_collect_assoc\<close>,	
 	       (*"[| l is_const; m is_const |] ==>  
                                        l * n + (m * n + k) =  (l + m) * n + k"*)
 	       \<^rule_thm>\<open>real_one_collect\<close>,
 	       (*"m is_const ==> n + m * n = (1 + m) * n"*)
-	       Rule.Thm ("real_one_collect_assoc",
-                     ThmC.numerals_to_Free @{thm real_one_collect_assoc}), 
+	       \<^rule_thm>\<open>real_one_collect_assoc\<close>, 
 	       (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
 
 	       \<^rule_eval>\<open>plus\<close> (eval_binop "#add_"), 
diff -r 73e7175a7d3f -r 09106b85d3b4 src/Tools/isac/Knowledge/PolyEq.thy
--- a/src/Tools/isac/Knowledge/PolyEq.thy	Sat Jun 12 18:06:27 2021 +0200
+++ b/src/Tools/isac/Knowledge/PolyEq.thy	Sat Jun 12 18:22:07 2021 +0200
@@ -439,9 +439,7 @@
        erls = PolyEq_erls,
        srls = Rule_Set.Empty, 
        calc = [], errpatts = [],
-       rules = [\<^rule_thm>\<open>d0_true\<close>,
-		Rule.Thm("d0_false",ThmC.numerals_to_Free @{thm  d0_false})
-		],
+       rules = [\<^rule_thm>\<open>d0_true\<close>, \<^rule_thm>\<open>d0_false\<close>],
        scr = Rule.Empty_Prog
        });
 
@@ -1305,8 +1303,7 @@
 		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
 		\<^rule_thm>\<open>separate_1_bdv_n\<close>,
 		(*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?n"*)
-		Rule.Thm ("add_divide_distrib", 
-		     ThmC.numerals_to_Free @{thm add_divide_distrib})
+		\<^rule_thm>\<open>add_divide_distrib\<close>
 		(*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
 		      WN051031 DOES NOT BELONG TO HERE*)
 		];
diff -r 73e7175a7d3f -r 09106b85d3b4 src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Sat Jun 12 18:06:27 2021 +0200
+++ b/src/Tools/isac/Knowledge/Rational.thy	Sat Jun 12 18:22:07 2021 +0200
@@ -660,11 +660,9 @@
 	       (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
 		     and does not commute a / b * c  \<up>  2 !*)
 	       
-	       Rule.Thm ("divide_divide_eq_right", 
-                     ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
+	       \<^rule_thm>\<open>divide_divide_eq_right\<close>,
 	       (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
-	       Rule.Thm ("divide_divide_eq_left",
-                     ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
+	       \<^rule_thm>\<open>divide_divide_eq_left\<close>,
 	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
 	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
 	       ],
diff -r 73e7175a7d3f -r 09106b85d3b4 src/Tools/isac/Knowledge/RootEq.thy
--- a/src/Tools/isac/Knowledge/RootEq.thy	Sat Jun 12 18:06:27 2021 +0200
+++ b/src/Tools/isac/Knowledge/RootEq.thy	Sat Jun 12 18:22:07 2021 +0200
@@ -223,67 +223,49 @@
             (* sqrt a sqrt b -> sqrt(ab) *)
        \<^rule_thm>\<open>sqrt_times_root_2\<close>,
             (* a sqrt b sqrt c -> a sqrt(bc) *)
-       Rule.Thm("sqrt_square_equation_both_1",
-           ThmC.numerals_to_Free @{thm sqrt_square_equation_both_1}),
+       \<^rule_thm>\<open>sqrt_square_equation_both_1\<close>,
        (* (sqrt a + sqrt b  = sqrt c + sqrt d) -> 
             (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
-       Rule.Thm("sqrt_square_equation_both_2",
-            ThmC.numerals_to_Free @{thm sqrt_square_equation_both_2}),
+       \<^rule_thm>\<open>sqrt_square_equation_both_2\<close>,
        (* (sqrt a - sqrt b  = sqrt c + sqrt d) -> 
             (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
-       Rule.Thm("sqrt_square_equation_both_3",
-            ThmC.numerals_to_Free @{thm sqrt_square_equation_both_3}),
+       \<^rule_thm>\<open>sqrt_square_equation_both_3\<close>,
        (* (sqrt a + sqrt b  = sqrt c - sqrt d) -> 
             (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
-       Rule.Thm("sqrt_square_equation_both_4",
-            ThmC.numerals_to_Free @{thm sqrt_square_equation_both_4}),
+       \<^rule_thm>\<open>sqrt_square_equation_both_4\<close>,
        (* (sqrt a - sqrt b  = sqrt c - sqrt d) -> 
             (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
-       Rule.Thm("sqrt_isolate_l_add1",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add1}), 
+       \<^rule_thm>\<open>sqrt_isolate_l_add1\<close>, 
        (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
-       Rule.Thm("sqrt_isolate_l_add2",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add2}), 
+       \<^rule_thm>\<open>sqrt_isolate_l_add2\<close>, 
        (* a+  sqrt(x)=d ->   sqrt(x) = d-a *)
-       Rule.Thm("sqrt_isolate_l_add3",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add3}), 
+       \<^rule_thm>\<open>sqrt_isolate_l_add3\<close>, 
        (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
-       Rule.Thm("sqrt_isolate_l_add4",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add4}), 
+       \<^rule_thm>\<open>sqrt_isolate_l_add4\<close>, 
        (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
-       Rule.Thm("sqrt_isolate_l_add5",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add5}), 
+       \<^rule_thm>\<open>sqrt_isolate_l_add5\<close>, 
        (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
-       Rule.Thm("sqrt_isolate_l_add6",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_l_add6}), 
+       \<^rule_thm>\<open>sqrt_isolate_l_add6\<close>, 
        (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
        (*\<^rule_thm>\<open>sqrt_isolate_l_div\<close>,*)
          (* b*sqrt(x) = d sqrt(x) d/b *)
-       Rule.Thm("sqrt_isolate_r_add1",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add1}),
+       \<^rule_thm>\<open>sqrt_isolate_r_add1\<close>,
        (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
-       Rule.Thm("sqrt_isolate_r_add2",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add2}),
+       \<^rule_thm>\<open>sqrt_isolate_r_add2\<close>,
        (* a= d+  sqrt(x) -> a-d=  sqrt(x) *)
-       Rule.Thm("sqrt_isolate_r_add3",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add3}),
+       \<^rule_thm>\<open>sqrt_isolate_r_add3\<close>,
        (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
-       Rule.Thm("sqrt_isolate_r_add4",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add4}),
+       \<^rule_thm>\<open>sqrt_isolate_r_add4\<close>,
        (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
-       Rule.Thm("sqrt_isolate_r_add5",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add5}),
+       \<^rule_thm>\<open>sqrt_isolate_r_add5\<close>,
        (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
-       Rule.Thm("sqrt_isolate_r_add6",
-            ThmC.numerals_to_Free @{thm sqrt_isolate_r_add6}),
+       \<^rule_thm>\<open>sqrt_isolate_r_add6\<close>,
        (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
        (*\<^rule_thm>\<open>sqrt_isolate_r_div\<close>,*)
          (* a=e*sqrt(x) -> a/e = sqrt(x) *)
-       Rule.Thm("sqrt_square_equation_left_1",
-            ThmC.numerals_to_Free @{thm sqrt_square_equation_left_1}),   
+       \<^rule_thm>\<open>sqrt_square_equation_left_1\<close>,   
        (* sqrt(x)=b -> x=b^2 *)
-       Rule.Thm("sqrt_square_equation_left_2",
-            ThmC.numerals_to_Free @{thm sqrt_square_equation_left_2}),   
+       \<^rule_thm>\<open>sqrt_square_equation_left_2\<close>,   
        (* c*sqrt(x)=b -> c^2*x=b^2 *)
        \<^rule_thm>\<open>sqrt_square_equation_left_3\<close>,  
 	      (* c/sqrt(x)=b -> c^2/x=b^2 *)
diff -r 73e7175a7d3f -r 09106b85d3b4 test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy
--- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy	Sat Jun 12 18:06:27 2021 +0200
+++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2.thy	Sat Jun 12 18:22:07 2021 +0200
@@ -2,7 +2,7 @@
 
 ML \<open>val test_list_rls =
   Rule_Set.append_rules "test_list_rls" Rule_Set.empty
-    [Rule.Thm ("refl", @{thm refl}), Rule.Thm ("subst", @{thm subst})]\<close>
+    [\<^rule_thm>\<open>refl\<close>, \<^rule_thm>\<open>subst\<close>]\<close>
 
 setup \<open>Test_KEStore_Elems.add_rlss 
   [("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*)
diff -r 73e7175a7d3f -r 09106b85d3b4 test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy
--- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy	Sat Jun 12 18:06:27 2021 +0200
+++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_2b.thy	Sat Jun 12 18:22:07 2021 +0200
@@ -1,7 +1,7 @@
 theory Thy_2b imports Thy_1 begin
 
 ML \<open>val test_list_rls =
-  Rule_Set.append_rules "test_list_rls" Rule_Set.empty [Rule.Thm ("False_def", @{thm False_def})]\<close>
+  Rule_Set.append_rules "test_list_rls" Rule_Set.empty [\<^rule_thm>\<open>False_def\<close>]\<close>
 
 setup \<open>Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory},
   test_list_rls))]\<close>
diff -r 73e7175a7d3f -r 09106b85d3b4 test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy
--- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy	Sat Jun 12 18:06:27 2021 +0200
+++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_3.thy	Sat Jun 12 18:22:07 2021 +0200
@@ -1,7 +1,7 @@
 theory Thy_3 imports Thy_2 Thy_2b begin
 
 ML \<open>val test_list_rls =
-  Rule_Set.append_rules "test_list_rls" Rule_Set.empty [Rule.Thm ("not_def", @{thm not_def})]\<close>
+  Rule_Set.append_rules "test_list_rls" Rule_Set.empty [\<^rule_thm>\<open>not_def\<close>]\<close>
 
 setup \<open>Test_KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*)
   [("test_list_rls", (Context.theory_name @{theory}, test_list_rls))]\<close>
diff -r 73e7175a7d3f -r 09106b85d3b4 test/Tools/isac/ProgLang/auto_prog.sml
--- a/test/Tools/isac/ProgLang/auto_prog.sml	Sat Jun 12 18:06:27 2021 +0200
+++ b/test/Tools/isac/ProgLang/auto_prog.sml	Sat Jun 12 18:22:07 2021 +0200
@@ -221,7 +221,7 @@
 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
 "-------- fun rules2scr_Rls --------------------------------------------------------------------";
 (*compare Prog_Expr.*)
-val prog = Auto_Prog.rules2scr_Rls @{theory} [Rule.Thm ("thm111", @{thm thm111}), Rule.Thm ("refl", @{thm refl})]
+val prog = Auto_Prog.rules2scr_Rls @{theory} [\<^rule_thm>\<open>thm111\<close>, \<^rule_thm>\<open>refl\<close>]
 ;
 writeln (UnparseC.term_in_thy @{theory} prog);
 (*auto_generated t_t =