1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Sat Jun 12 18:06:27 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Sat Jun 12 18:22:07 2021 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4  		     rules = [(*for rewriting conditions in Thm's*)
     1.5  			      \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
     1.6  			      \<^rule_thm>\<open>not_true\<close>,
     1.7 -			      Rule.Thm ("not_false",@{thm not_false})
     1.8 +			      \<^rule_thm>\<open>not_false\<close>
     1.9  			      ],
    1.10  		     scr = Rule.Empty_Prog}, 
    1.11  	 srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.12 @@ -179,14 +179,11 @@
    1.13  	       \<^rule_thm>\<open>rat_mult_poly_r\<close>,
    1.14  	       (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
    1.15  
    1.16 -	       Rule.Thm ("real_divide_divide1_mg",
    1.17 -                     ThmC.numerals_to_Free @{thm real_divide_divide1_mg}),
    1.18 +	       \<^rule_thm>\<open>real_divide_divide1_mg\<close>,
    1.19  	       (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
    1.20 -	       Rule.Thm ("divide_divide_eq_right", 
    1.21 -                     ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
    1.22 +	       \<^rule_thm>\<open>divide_divide_eq_right\<close>,
    1.23  	       (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
    1.24 -	       Rule.Thm ("divide_divide_eq_left",
    1.25 -                     ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
    1.26 +	       \<^rule_thm>\<open>divide_divide_eq_left\<close>,
    1.27  	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
    1.28  	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    1.29  	      
    1.30 @@ -233,8 +230,7 @@
    1.31  		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)
    1.32  		\<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
    1.33  			  (*"?bdv  \<up>  ?n / ?b = 1 / ?b * ?bdv  \<up>  ?n"*)
    1.34 -			  *****Rule.Thm ("add_divide_distrib", 
    1.35 -			  ***** ThmC.numerals_to_Free @{thm add_divide_distrib})
    1.36 +			  *****\<^rule_thm>\<open>add_divide_distrib\<close>
    1.37  			  (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
    1.38  		];
    1.39  val simplify_Integral = 
    1.40 @@ -286,8 +282,7 @@
    1.41  * 			  (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
    1.42  * 			  \<^rule_thm>\<open>separate_1_bdv_n\<close>(*,
    1.43  * 			  (*"?bdv  \<up>  ?n / ?b = 1 / ?b * ?bdv  \<up>  ?n"*)
    1.44 -* 			  Rule.Thm ("add_divide_distrib", 
    1.45 -* 				  ThmC.numerals_to_Free @{thm add_divide_distrib})
    1.46 +* 			  \<^rule_thm>\<open>add_divide_distrib\<close>
    1.47  * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
    1.48  * 			  ]),
    1.49  * 	       \<^rule_eval>\<open>divide\<close> (eval_cancel "#divide_e")