1.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Mon Apr 13 13:27:55 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Mon Apr 13 15:31:23 2020 +0200
     1.3 @@ -88,12 +88,12 @@
     1.4  	      Rule.Num_Calc ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""),
     1.5  	      Rule.Num_Calc ("RatEq.is'_ratequation'_in", eval_is_ratequation_in ""),
     1.6  	      Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
     1.7 -	      Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
     1.8 -	      Rule.Thm ("not_false",TermC.num_str @{thm not_false}),
     1.9 -	      Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
    1.10 -	      Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
    1.11 -	      Rule.Thm ("or_true",TermC.num_str @{thm or_true}),
    1.12 -	      Rule.Thm ("or_false",TermC.num_str @{thm or_false})
    1.13 +	      Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
    1.14 +	      Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
    1.15 +	      Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
    1.16 +	      Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
    1.17 +	      Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
    1.18 +	      Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false})
    1.19  	      ];
    1.20  
    1.21  \<close> ML \<open>
    1.22 @@ -104,8 +104,8 @@
    1.23  		  (Rule_Set.append_rules "is_ratequation_in"
    1.24  			  Poly_erls [(*Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),*)
    1.25  			    Rule.Num_Calc ("RatEq.is'_ratequation'_in", eval_is_ratequation_in "")]))
    1.26 - [Rule.Thm ("and_commute",TermC.num_str @{thm and_commute}), (*WN: ein Hack*)
    1.27 -	Rule.Thm ("or_commute",TermC.num_str @{thm or_commute})];  (*WN: ein Hack*)
    1.28 + [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)
    1.29 +	Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})];  (*WN: ein Hack*)
    1.30  
    1.31  \<close> ML \<open>
    1.32  val RatEq_crls = 
    1.33 @@ -114,19 +114,19 @@
    1.34  		  (Rule_Set.append_rules "is_ratequation_in"
    1.35  			  Poly_erls [(*Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),*)
    1.36  			    Rule.Num_Calc ("RatEq.is'_ratequation'_in", eval_is_ratequation_in "")]))
    1.37 - [Rule.Thm ("and_commute",TermC.num_str @{thm and_commute}), (*WN: ein Hack*)
    1.38 -	Rule.Thm ("or_commute",TermC.num_str @{thm or_commute})];  (*WN: ein Hack*)
    1.39 + [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)
    1.40 +	Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})];  (*WN: ein Hack*)
    1.41  
    1.42  val RatEq_eliminate = prep_rls'(
    1.43    Rule_Def.Repeat
    1.44      {id = "RatEq_eliminate", preconds = [], rew_ord = ("termlessI", termlessI), erls = rateq_erls,
    1.45       srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.46       rules = [
    1.47 -	     Rule.Thm("rat_mult_denominator_both",TermC.num_str @{thm rat_mult_denominator_both}), 
    1.48 +	     Rule.Thm("rat_mult_denominator_both",ThmC.numerals_to_Free @{thm rat_mult_denominator_both}), 
    1.49  	     (* a/b=c/d -> ad=cb *)
    1.50 -	     Rule.Thm("rat_mult_denominator_left",TermC.num_str @{thm rat_mult_denominator_left}), 
    1.51 +	     Rule.Thm("rat_mult_denominator_left",ThmC.numerals_to_Free @{thm rat_mult_denominator_left}), 
    1.52  	     (* a  =c/d -> ad=c  *)
    1.53 -	     Rule.Thm("rat_mult_denominator_right",TermC.num_str @{thm rat_mult_denominator_right})
    1.54 +	     Rule.Thm("rat_mult_denominator_right",ThmC.numerals_to_Free @{thm rat_mult_denominator_right})
    1.55  	     (* a/b=c   ->  a=cb *)
    1.56  	     ],
    1.57      scr = Rule.EmptyScr});
    1.58 @@ -137,21 +137,21 @@
    1.59      {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI), erls = rateq_erls,
    1.60       srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.61       rules = [
    1.62 -	     Rule.Thm("real_rat_mult_1",TermC.num_str @{thm real_rat_mult_1}),
    1.63 +	     Rule.Thm("real_rat_mult_1",ThmC.numerals_to_Free @{thm real_rat_mult_1}),
    1.64  	     (*a*(b/c) = (a*b)/c*)
    1.65 -	     Rule.Thm("real_rat_mult_2",TermC.num_str @{thm real_rat_mult_2}),
    1.66 +	     Rule.Thm("real_rat_mult_2",ThmC.numerals_to_Free @{thm real_rat_mult_2}),
    1.67  	     (*(a/b)*(c/d) = (a*c)/(b*d)*)
    1.68 -       Rule.Thm("real_rat_mult_3",TermC.num_str @{thm real_rat_mult_3}),
    1.69 +       Rule.Thm("real_rat_mult_3",ThmC.numerals_to_Free @{thm real_rat_mult_3}),
    1.70         (* (a/b)*c = (a*c)/b*)
    1.71 -	     Rule.Thm("real_rat_pow",TermC.num_str @{thm real_rat_pow}),
    1.72 +	     Rule.Thm("real_rat_pow",ThmC.numerals_to_Free @{thm real_rat_pow}),
    1.73  	     (*(a/b)^^^2 = a^^^2/b^^^2*)
    1.74 -	     Rule.Thm("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
    1.75 +	     Rule.Thm("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
    1.76  	     (* a - b = a + (-1) * b *)
    1.77 -       Rule.Thm("rat_double_rat_1",TermC.num_str @{thm rat_double_rat_1}),
    1.78 +       Rule.Thm("rat_double_rat_1",ThmC.numerals_to_Free @{thm rat_double_rat_1}),
    1.79         (* (a / (c/d) = (a*d) / c) *)
    1.80 -       Rule.Thm("rat_double_rat_2",TermC.num_str @{thm rat_double_rat_2}), 
    1.81 +       Rule.Thm("rat_double_rat_2",ThmC.numerals_to_Free @{thm rat_double_rat_2}), 
    1.82         (* ((a/b) / (c/d) = (a*d) / (b*c)) *)
    1.83 -       Rule.Thm("rat_double_rat_3",TermC.num_str @{thm rat_double_rat_3}) 
    1.84 +       Rule.Thm("rat_double_rat_3",ThmC.numerals_to_Free @{thm rat_double_rat_3}) 
    1.85         (* ((a/b) / c = a / (b*c) ) *)],
    1.86       scr = Rule.EmptyScr});
    1.87  \<close>