1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Jun 10 17:06:32 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Fri Jun 11 11:49:34 2021 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4  		     erls = Rule_Set.Empty, 
     1.5  		     srls = Rule_Set.Empty, calc = [], errpatts = [],
     1.6  		     rules = [(*for rewriting conditions in Thm's*)
     1.7 -			      Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
     1.8 +			      \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "#occurs_in_"),
     1.9  			      Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
    1.10  			      Rule.Thm ("not_false",@{thm not_false})
    1.11  			      ],
    1.12 @@ -130,7 +130,7 @@
    1.13  		  Rule.Thm ("integral_add", ThmC.numerals_to_Free @{thm integral_add}),
    1.14  		  Rule.Thm ("integral_mult", ThmC.numerals_to_Free @{thm integral_mult}),
    1.15  		  Rule.Thm ("integral_pow", ThmC.numerals_to_Free @{thm integral_pow}),
    1.16 -		  Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")(*for n+1*)
    1.17 +		  \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")(*for n+1*)
    1.18  		  ],
    1.19  	 scr = Rule.Empty_Prog};
    1.20  \<close>
    1.21 @@ -143,9 +143,8 @@
    1.22  		     rew_ord = ("termlessI",termlessI), 
    1.23  		     erls = Rule_Set.Empty, 
    1.24  		     srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.25 -		     rules = [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches""),
    1.26 -			      Rule.Eval ("Integrate.is_f_x", 
    1.27 -				    eval_is_f_x "is_f_x_"),
    1.28 +		     rules = [\<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches""),
    1.29 +			      \<^rule_eval>\<open>Integrate.is_f_x\<close> (eval_is_f_x "is_f_x_"),
    1.30  			      Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
    1.31  			      Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})
    1.32  			      ],
    1.33 @@ -171,8 +170,7 @@
    1.34  		       rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), 
    1.35  		       erls = (*FIXME.WN051028 Rule_Set.empty,*)
    1.36  		       Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
    1.37 -				  [Rule.Eval ("Poly.is_polyexp", 
    1.38 -					 eval_is_polyexp "")],
    1.39 +				  [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
    1.40  				  srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.41  				  rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
    1.42  	       (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
    1.43 @@ -190,7 +188,7 @@
    1.44  	       Rule.Thm ("divide_divide_eq_left",
    1.45                       ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
    1.46  	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
    1.47 -	       Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
    1.48 +	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
    1.49  	      
    1.50  	       Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
    1.51  		(*"(?a / ?b)  \<up>  ?n = ?a  \<up>  ?n / ?b  \<up>  ?n"*)
    1.52 @@ -254,7 +252,7 @@
    1.53  	       Rule.Rls_ discard_parentheses,
    1.54  	       (*Rule.Rls_ collect_bdv, from make_polynomial_in*)
    1.55  	       Rule.Rls_ separate_bdv2,
    1.56 -	       Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
    1.57 +	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
    1.58  	       ],
    1.59        scr = Rule.Empty_Prog};      
    1.60  
    1.61 @@ -292,7 +290,7 @@
    1.62  * 				  ThmC.numerals_to_Free @{thm add_divide_distrib})
    1.63  * 			   (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
    1.64  * 			  ]),
    1.65 -* 	       Rule.Eval ("Rings.divide_class.divide"  , eval_cancel "#divide_e")
    1.66 +* 	       \<^rule_eval>\<open>divide\<close> (eval_cancel "#divide_e")
    1.67  * 	       ],
    1.68  *       scr = Rule.Empty_Prog
    1.69  *       });