1.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy	Sat Jun 12 14:27:03 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy	Sat Jun 12 14:29:10 2021 +0200
     1.3 @@ -64,25 +64,25 @@
     1.4  \<close> ML \<open>
     1.5  val Atools_erls = Rule_Set.append_rules "Atools_erls" Rule_Set.empty
     1.6    [ \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
     1.7 -    Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
     1.8 +    \<^rule_thm>\<open>not_true\<close>,
     1.9  		(*"(~ True) = False"*)
    1.10 -		Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
    1.11 +		\<^rule_thm>\<open>not_false\<close>,
    1.12  		(*"(~ False) = True"*)
    1.13 -		Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
    1.14 +		\<^rule_thm>\<open>and_true\<close>,
    1.15  		(*"(?a & True) = ?a"*)
    1.16 -		Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
    1.17 +		\<^rule_thm>\<open>and_false\<close>,
    1.18  		(*"(?a & False) = False"*)
    1.19 -		Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
    1.20 +		\<^rule_thm>\<open>or_true\<close>,
    1.21  		(*"(?a | True) = True"*)
    1.22 -		Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
    1.23 +		\<^rule_thm>\<open>or_false\<close>,
    1.24  		(*"(?a | False) = ?a"*)
    1.25                 
    1.26 -		Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
    1.27 -		Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),
    1.28 -		Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3}),
    1.29 -      Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),
    1.30 -		Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
    1.31 -		Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
    1.32 +		\<^rule_thm>\<open>rat_leq1\<close>,
    1.33 +		\<^rule_thm>\<open>rat_leq2\<close>,
    1.34 +		\<^rule_thm>\<open>rat_leq3\<close>,
    1.35 +    \<^rule_thm>\<open>refl\<close>,
    1.36 +		\<^rule_thm>\<open>order_refl\<close>,
    1.37 +		\<^rule_thm>\<open>radd_left_cancel_le\<close>,
    1.38  		
    1.39  		\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
    1.40  		\<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
    1.41 @@ -96,19 +96,19 @@
    1.42  ML \<open>
    1.43  val Atools_crls = Rule_Set.append_rules "Atools_crls" Rule_Set.empty
    1.44    [ \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
    1.45 -    Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
    1.46 -		Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
    1.47 -		Rule.Thm ("and_true", ThmC.numerals_to_Free @{thm and_true}),
    1.48 -		Rule.Thm ("and_false", ThmC.numerals_to_Free @{thm and_false}),
    1.49 -		Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
    1.50 -		Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
    1.51 -               
    1.52 -		Rule.Thm ("rat_leq1", ThmC.numerals_to_Free @{thm rat_leq1}),
    1.53 -		Rule.Thm ("rat_leq2", ThmC.numerals_to_Free @{thm rat_leq2}),
    1.54 -		Rule.Thm ("rat_leq3", ThmC.numerals_to_Free @{thm rat_leq3}),
    1.55 -		Rule.Thm ("refl", ThmC.numerals_to_Free @{thm refl}),
    1.56 -		Rule.Thm ("order_refl", ThmC.numerals_to_Free @{thm order_refl}),
    1.57 -		Rule.Thm ("radd_left_cancel_le", ThmC.numerals_to_Free @{thm radd_left_cancel_le}),
    1.58 +    \<^rule_thm>\<open>not_true\<close>,
    1.59 +		\<^rule_thm>\<open>not_false\<close>,
    1.60 +		\<^rule_thm>\<open>and_true\<close>,
    1.61 +		\<^rule_thm>\<open>and_false\<close>,
    1.62 +		\<^rule_thm>\<open>or_true\<close>,
    1.63 +		\<^rule_thm>\<open>or_false\<close>,
    1.64 +
    1.65 +		\<^rule_thm>\<open>rat_leq1\<close>,
    1.66 +		\<^rule_thm>\<open>rat_leq2\<close>,
    1.67 +		\<^rule_thm>\<open>rat_leq3\<close>,
    1.68 +		\<^rule_thm>\<open>refl\<close>,
    1.69 +		\<^rule_thm>\<open>order_refl\<close>,
    1.70 +		\<^rule_thm>\<open>radd_left_cancel_le\<close>,
    1.71  		
    1.72  		\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
    1.73  		\<^rule_eval>\<open>less_eq\<close> (Prog_Expr.eval_equ "#less_equal_"),
    1.74 @@ -132,8 +132,8 @@
    1.75         
    1.76  		\<^rule_eval>\<open>Prog_Expr.Vars\<close> (Prog_Expr.eval_var "#Vars_"),
    1.77  		
    1.78 -		Rule.Thm ("if_True",ThmC.numerals_to_Free @{thm if_True}),
    1.79 -		Rule.Thm ("if_False",ThmC.numerals_to_Free @{thm if_False})];
    1.80 +		\<^rule_thm>\<open>if_True\<close>,
    1.81 +		\<^rule_thm>\<open>if_False\<close>];
    1.82  
    1.83  val prog_expr = Auto_Prog.prep_rls @{theory} (Rule_Set.merge "list_erls"
    1.84  	(Rule_Def.Repeat {id = "replaced", preconds = [], rew_ord = ("termlessI", termlessI),