1.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Thu Jun 10 17:06:32 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Fri Jun 11 11:49:34 2021 +0200
     1.3 @@ -80,12 +80,12 @@
     1.4  ML \<open>
     1.5  val RatEq_prls = (*15.10.02:just the following order due to subterm evaluation*)
     1.6    Rule_Set.append_rules "RatEq_prls" Rule_Set.empty 
     1.7 -	     [Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
     1.8 -	      Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
     1.9 -	      Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs ""),
    1.10 -	      Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""),
    1.11 -	      Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in ""),
    1.12 -	      Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
    1.13 +	     [\<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
    1.14 +	      \<^rule_eval>\<open>Prog_Expr.matches\<close> (Prog_Expr.eval_matches ""),
    1.15 +	      \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs ""),
    1.16 +	      \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs ""),
    1.17 +	      \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in ""),
    1.18 +	      \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
    1.19  	      Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
    1.20  	      Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
    1.21  	      Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
    1.22 @@ -100,8 +100,8 @@
    1.23    Rule_Set.keep_unique_rules "rateq_erls"                             (*WN: ein Hack*)
    1.24  	  (Rule_Set.merge "is_ratequation_in" calculate_Rational
    1.25  		  (Rule_Set.append_rules "is_ratequation_in"
    1.26 -			  Poly_erls [(*Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),*)
    1.27 -			    Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in "")]))
    1.28 +			  Poly_erls [(*\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),*)
    1.29 +			    \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in "")]))
    1.30   [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)
    1.31  	Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})];  (*WN: ein Hack*)
    1.32  
    1.33 @@ -110,8 +110,8 @@
    1.34    Rule_Set.keep_unique_rules "RatEq_crls"                              (*WN: ein Hack*)
    1.35  	  (Rule_Set.merge "is_ratequation_in" calculate_Rational
    1.36  		  (Rule_Set.append_rules "is_ratequation_in"
    1.37 -			  Poly_erls [(*Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),*)
    1.38 -			    Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in "")]))
    1.39 +			  Poly_erls [(*\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),*)
    1.40 +			    \<^rule_eval>\<open>is_ratequation_in\<close> (eval_is_ratequation_in "")]))
    1.41   [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)
    1.42  	Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})];  (*WN: ein Hack*)
    1.43