1.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -739,8 +739,8 @@
     1.4  	       Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
     1.5  	       Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"),
     1.6  	       Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
     1.7 -	       Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
     1.8 -	       Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
     1.9 +	       Rule.Thm ("not_false",  @{thm not_false}),
    1.10 +	       Rule.Thm ("not_true",  @{thm not_true}),
    1.11  	       Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
    1.12  	       ],
    1.13        scr = Rule.Empty_Prog
    1.14 @@ -753,7 +753,7 @@
    1.15        rules =
    1.16         [\<^rule_thm>\<open>real_diff_minus\<close>,
    1.17            (*"a - b = a + -1 * b"*)
    1.18 -        Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym}))
    1.19 +        Rule.Thm ("real_mult_minus1_sym",  (@{thm real_mult_minus1_sym}))
    1.20  	        (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)],
    1.21  	      scr = Rule.Empty_Prog};
    1.22  
    1.23 @@ -790,9 +790,9 @@
    1.24  	         \<^rule_thm>\<open>realpow_pow\<close>,
    1.25  	           (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
    1.26  (**)
    1.27 -	         Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}),
    1.28 +	         Rule.Thm ("realpow_minus_even", @{thm realpow_minus_even}),
    1.29  	           (*"n is_even ==> (- r) \<up> n = r \<up> n"*)
    1.30 -	         Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd})
    1.31 +	         Rule.Thm ("realpow_minus_odd", @{thm realpow_minus_odd})
    1.32  	           (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
    1.33  (**)
    1.34  	       ], scr = Rule.Empty_Prog};
    1.35 @@ -803,8 +803,8 @@
    1.36        erls =  Rule_Set.append_rules "Rule_Set.empty-expand_poly_rat_" Rule_Set.empty
    1.37  	        [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""),
    1.38  	         Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"),
    1.39 -	         Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
    1.40 -	         Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true})
    1.41 +	         Rule.Thm ("not_false",  @{thm not_false}),
    1.42 +	         Rule.Thm ("not_true",  @{thm not_true})
    1.43  		      ],
    1.44        srls = Rule_Set.Empty,
    1.45        calc = [], errpatts = [],
    1.46 @@ -832,11 +832,11 @@
    1.47  	 \<^rule_thm>\<open>realpow_multI_poly\<close>,
    1.48  	     (*"[| r is_polyexp; s is_polyexp |] ==> 
    1.49  		            (r * s) \<up> n = r \<up> n * s \<up> n"*)
    1.50 -	 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
    1.51 +	 Rule.Thm ("realpow_pow", @{thm realpow_pow}),
    1.52  	   (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
    1.53 -	 Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}),
    1.54 +	 Rule.Thm ("realpow_minus_even", @{thm realpow_minus_even}),
    1.55  	   (*"n is_even ==> (- r) \<up> n = r \<up> n"*)
    1.56 -	 Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd})
    1.57 +	 Rule.Thm ("realpow_minus_odd", @{thm realpow_minus_odd})
    1.58  	   (*"\<not> (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
    1.59  	 ], scr = Rule.Empty_Prog};
    1.60  
    1.61 @@ -962,11 +962,11 @@
    1.62        rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    1.63        erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.64        rules = 
    1.65 -        [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
    1.66 +        [Rule.Thm ("distrib_right" , @{thm distrib_right}),
    1.67  	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
    1.68  	       \<^rule_thm>\<open>distrib_left\<close>,
    1.69  	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
    1.70 -	       (*Rule.Thm ("distrib_right1",ThmC.numerals_to_Free @{thm distrib_right}1),
    1.71 +	       (*Rule.Thm ("distrib_right1", @{thm distrib_right}1),
    1.72  		....... 18.3.03 undefined???*)
    1.73  
    1.74  	       \<^rule_thm>\<open>real_plus_binom_pow2\<close>,
    1.75 @@ -982,7 +982,7 @@
    1.76  	       (*"- (- ?z) = ?z"*)
    1.77  	       \<^rule_thm>\<open>real_diff_minus\<close>,
    1.78  	       (*"a - b = a + -1 * b"*)
    1.79 -	       Rule.Thm ("real_mult_minus1_sym", ThmC.numerals_to_Free (@{thm real_mult_minus1_sym}))
    1.80 +	       Rule.Thm ("real_mult_minus1_sym",  (@{thm real_mult_minus1_sym}))
    1.81  	       (*"\<not>(z is_const) ==> - (z::real) = -1 * z"*)
    1.82  
    1.83  	       (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*)
    1.84 @@ -1043,7 +1043,7 @@
    1.85  	       (*"1 * z = z"*)
    1.86  	       (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*)
    1.87  	       (*"-1 * z = - z"*)
    1.88 -	       Rule.Thm ("minus_mult_left", ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),
    1.89 +	       Rule.Thm ("minus_mult_left",  (@{thm minus_mult_left} RS @{thm sym})),
    1.90  	       (*- (?x * ?y) = "- ?x * ?y"*)
    1.91  	       (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>,
    1.92  	       (*"- ?x * - ?y = ?x * ?y"*)---*)