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")