1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Apr 13 13:27:55 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Apr 13 15:31:23 2020 +0200
1.3 @@ -395,8 +395,8 @@
1.4 rules =
1.5 [Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
1.6 Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
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 ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.10 + Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
1.11 scr = Rule.EmptyScr});
1.12
1.13 (* simplifies expressions with numerals;
1.14 @@ -410,39 +410,39 @@
1.15 rules =
1.16 [Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.17
1.18 - Rule.Thm ("minus_divide_left", TermC.num_str (@{thm minus_divide_left} RS @{thm sym})),
1.19 + Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
1.20 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
1.21 - Rule.Thm ("rat_add", TermC.num_str @{thm rat_add}),
1.22 + Rule.Thm ("rat_add", ThmC.numerals_to_Free @{thm rat_add}),
1.23 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
1.24 \a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
1.25 - Rule.Thm ("rat_add1", TermC.num_str @{thm rat_add1}),
1.26 + Rule.Thm ("rat_add1", ThmC.numerals_to_Free @{thm rat_add1}),
1.27 (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
1.28 - Rule.Thm ("rat_add2", TermC.num_str @{thm rat_add2}),
1.29 + Rule.Thm ("rat_add2", ThmC.numerals_to_Free @{thm rat_add2}),
1.30 (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
1.31 - Rule.Thm ("rat_add3", TermC.num_str @{thm rat_add3}),
1.32 + Rule.Thm ("rat_add3", ThmC.numerals_to_Free @{thm rat_add3}),
1.33 (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c"\
1.34 .... is_const to be omitted here FIXME*)
1.35
1.36 - Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.37 + Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
1.38 (*a / b * (c / d) = a * c / (b * d)*)
1.39 - Rule.Thm ("times_divide_eq_right", TermC.num_str @{thm times_divide_eq_right}),
1.40 + Rule.Thm ("times_divide_eq_right", ThmC.numerals_to_Free @{thm times_divide_eq_right}),
1.41 (*?x * (?y / ?z) = ?x * ?y / ?z*)
1.42 - Rule.Thm ("times_divide_eq_left", TermC.num_str @{thm times_divide_eq_left}),
1.43 + Rule.Thm ("times_divide_eq_left", ThmC.numerals_to_Free @{thm times_divide_eq_left}),
1.44 (*?y / ?z * ?x = ?y * ?x / ?z*)
1.45
1.46 - Rule.Thm ("real_divide_divide1", TermC.num_str @{thm real_divide_divide1}),
1.47 + Rule.Thm ("real_divide_divide1", ThmC.numerals_to_Free @{thm real_divide_divide1}),
1.48 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
1.49 - Rule.Thm ("divide_divide_eq_left", TermC.num_str @{thm divide_divide_eq_left}),
1.50 + Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.51 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.52
1.53 - Rule.Thm ("rat_power", TermC.num_str @{thm rat_power}),
1.54 + Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}),
1.55 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.56
1.57 - Rule.Thm ("mult_cross", TermC.num_str @{thm mult_cross}),
1.58 + Rule.Thm ("mult_cross", ThmC.numerals_to_Free @{thm mult_cross}),
1.59 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
1.60 - Rule.Thm ("mult_cross1", TermC.num_str @{thm mult_cross1}),
1.61 + Rule.Thm ("mult_cross1", ThmC.numerals_to_Free @{thm mult_cross1}),
1.62 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
1.63 - Rule.Thm ("mult_cross2", TermC.num_str @{thm mult_cross2})
1.64 + Rule.Thm ("mult_cross2", ThmC.numerals_to_Free @{thm mult_cross2})
1.65 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
1.66 scr = Rule.EmptyScr})
1.67 calculate_Poly);
1.68 @@ -478,7 +478,7 @@
1.69 val SOME (t'', asm) = cancel_p_ thy t;
1.70 val der = Rtools.reverse_deriv thy eval_rls rules ro NONE t';
1.71 val der = der @
1.72 - [(Rule.Thm ("real_mult_div_cancel2", TermC.num_str @{thm real_mult_div_cancel2}), (t'', asm))]
1.73 + [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))]
1.74 val rs = (Rtools.distinct_Thm o (map #1)) der
1.75 val rs = filter_out (Rtools.eq_Thms
1.76 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
1.77 @@ -539,7 +539,7 @@
1.78 val SOME (t'', asm) = add_fraction_p_ thy t;
1.79 val der = Rtools.reverse_deriv thy eval_rls rules ro NONE t';
1.80 val der = der @
1.81 - [(Rule.Thm ("real_mult_div_cancel2", TermC.num_str @{thm real_mult_div_cancel2}), (t'',asm))]
1.82 + [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))]
1.83 val rs = (Rtools.distinct_Thm o (map #1)) der;
1.84 val rs = filter_out (Rtools.eq_Thms
1.85 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
1.86 @@ -606,8 +606,8 @@
1.87 rules = [Rule.Num_Calc ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"),
1.88 Rule.Num_Calc ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_"),
1.89 Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.90 - Rule.Thm ("not_false", TermC.num_str @{thm not_false}),
1.91 - Rule.Thm ("not_true", TermC.num_str @{thm not_true}),
1.92 + Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
1.93 + Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
1.94 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.95 ],
1.96 scr = Rule.EmptyScr
1.97 @@ -617,29 +617,29 @@
1.98 val powers = prep_rls'(
1.99 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.100 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.101 - rules = [Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
1.102 + rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
1.103 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1.104 - Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow}),
1.105 + Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
1.106 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
1.107 - Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
1.108 + Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
1.109 (*"r ^^^ 1 = r"*)
1.110 - Rule.Thm ("realpow_minus_even",TermC.num_str @{thm realpow_minus_even}),
1.111 + Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}),
1.112 (*"n is_even ==> (- r) ^^^ n = r ^^^ n" ?-->discard_minus?*)
1.113 - Rule.Thm ("realpow_minus_odd",TermC.num_str @{thm realpow_minus_odd}),
1.114 + Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}),
1.115 (*"Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"*)
1.116
1.117 (*----- collect atoms over * -----*)
1.118 - Rule.Thm ("realpow_two_atom",TermC.num_str @{thm realpow_two_atom}),
1.119 + Rule.Thm ("realpow_two_atom",ThmC.numerals_to_Free @{thm realpow_two_atom}),
1.120 (*"r is_atom ==> r * r = r ^^^ 2"*)
1.121 - Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
1.122 + Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
1.123 (*"r is_atom ==> r * r ^^^ n = r ^^^ (n + 1)"*)
1.124 - Rule.Thm ("realpow_addI_atom",TermC.num_str @{thm realpow_addI_atom}),
1.125 + Rule.Thm ("realpow_addI_atom",ThmC.numerals_to_Free @{thm realpow_addI_atom}),
1.126 (*"r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
1.127
1.128 (*----- distribute none-atoms -----*)
1.129 - Rule.Thm ("realpow_def_atom",TermC.num_str @{thm realpow_def_atom}),
1.130 + Rule.Thm ("realpow_def_atom",ThmC.numerals_to_Free @{thm realpow_def_atom}),
1.131 (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)
1.132 - Rule.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI}),
1.133 + Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
1.134 (*"1 ^^^ n = 1"*)
1.135 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.136 ],
1.137 @@ -650,20 +650,20 @@
1.138 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
1.139 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.140 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.141 - rules = [Rule.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
1.142 + rules = [Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
1.143 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.144 - Rule.Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
1.145 + Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
1.146 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.147 otherwise inv.to a / b / c = ...*)
1.148 - Rule.Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),
1.149 + Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
1.150 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x^^^n too much
1.151 and does not commute a / b * c ^^^ 2 !*)
1.152
1.153 Rule.Thm ("divide_divide_eq_right",
1.154 - TermC.num_str @{thm divide_divide_eq_right}),
1.155 + ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
1.156 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.157 Rule.Thm ("divide_divide_eq_left",
1.158 - TermC.num_str @{thm divide_divide_eq_left}),
1.159 + ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.160 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.161 Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.162 ],
1.163 @@ -674,29 +674,29 @@
1.164 val reduce_0_1_2 = prep_rls'(
1.165 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.166 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.167 - rules = [(*Rule.Thm ("divide_1",TermC.num_str @{thm divide_1}),
1.168 + rules = [(*Rule.Thm ("divide_1",ThmC.numerals_to_Free @{thm divide_1}),
1.169 "?x / 1 = ?x" unnecess.for normalform*)
1.170 - Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1.171 + Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
1.172 (*"1 * z = z"*)
1.173 - (*Rule.Thm ("real_mult_minus1",TermC.num_str @{thm real_mult_minus1}),
1.174 + (*Rule.Thm ("real_mult_minus1",ThmC.numerals_to_Free @{thm real_mult_minus1}),
1.175 "-1 * z = - z"*)
1.176 - (*Rule.Thm ("real_minus_mult_cancel",TermC.num_str @{thm real_minus_mult_cancel}),
1.177 + (*Rule.Thm ("real_minus_mult_cancel",ThmC.numerals_to_Free @{thm real_minus_mult_cancel}),
1.178 "- ?x * - ?y = ?x * ?y"*)
1.179
1.180 - Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1.181 + Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
1.182 (*"0 * z = 0"*)
1.183 - Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
1.184 + Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
1.185 (*"0 + z = z"*)
1.186 - (*Rule.Thm ("right_minus",TermC.num_str @{thm right_minus}),
1.187 + (*Rule.Thm ("right_minus",ThmC.numerals_to_Free @{thm right_minus}),
1.188 "?z + - ?z = 0"*)
1.189
1.190 Rule.Thm ("sym_real_mult_2",
1.191 - TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
1.192 + ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
1.193 (*"z1 + z1 = 2 * z1"*)
1.194 - Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1.195 + Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
1.196 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.197
1.198 - Rule.Thm ("division_ring_divide_zero",TermC.num_str @{thm division_ring_divide_zero})
1.199 + Rule.Thm ("division_ring_divide_zero",ThmC.numerals_to_Free @{thm division_ring_divide_zero})
1.200 (*"0 / ?x = 0"*)
1.201 ], scr = Rule.EmptyScr});
1.202
1.203 @@ -741,20 +741,20 @@
1.204 val simplify_rational =
1.205 Rule_Set.merge "simplify_rational" expand_binoms
1.206 (Rule_Set.append_rules "divide" calculate_Rational
1.207 - [Rule.Thm ("div_by_1",TermC.num_str @{thm div_by_1}),
1.208 + [Rule.Thm ("div_by_1",ThmC.numerals_to_Free @{thm div_by_1}),
1.209 (*"?x / 1 = ?x"*)
1.210 - Rule.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
1.211 + Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
1.212 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.213 - Rule.Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
1.214 + Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
1.215 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
1.216 otherwise inv.to a / b / c = ...*)
1.217 - Rule.Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),
1.218 + Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
1.219 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
1.220 - Rule.Thm ("add_minus",TermC.num_str @{thm add_minus}),
1.221 + Rule.Thm ("add_minus",ThmC.numerals_to_Free @{thm add_minus}),
1.222 (*"?a + ?b - ?b = ?a"*)
1.223 - Rule.Thm ("add_minus1",TermC.num_str @{thm add_minus1}),
1.224 + Rule.Thm ("add_minus1",ThmC.numerals_to_Free @{thm add_minus1}),
1.225 (*"?a - ?b + ?b = ?a"*)
1.226 - Rule.Thm ("divide_minus1",TermC.num_str @{thm divide_minus1})
1.227 + Rule.Thm ("divide_minus1",ThmC.numerals_to_Free @{thm divide_minus1})
1.228 (*"?x / -1 = - ?x"*)
1.229 ]);
1.230 \<close>
1.231 @@ -780,9 +780,9 @@
1.232 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [Rule.Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.233 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.234 rules =
1.235 - [Rule.Thm ("rat_mult_poly_l",TermC.num_str @{thm rat_mult_poly_l}),
1.236 + [Rule.Thm ("rat_mult_poly_l",ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
1.237 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.238 - Rule.Thm ("rat_mult_poly_r",TermC.num_str @{thm rat_mult_poly_r})
1.239 + Rule.Thm ("rat_mult_poly_r",ThmC.numerals_to_Free @{thm rat_mult_poly_r})
1.240 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) ],
1.241 scr = Rule.EmptyScr});
1.242
1.243 @@ -794,22 +794,22 @@
1.244 val rat_mult_div_pow = prep_rls'(
1.245 Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.246 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.247 - rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),
1.248 + rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
1.249 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
1.250 - Rule.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),
1.251 + Rule.Thm ("rat_mult_poly_l", ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
1.252 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
1.253 - Rule.Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}),
1.254 + Rule.Thm ("rat_mult_poly_r", ThmC.numerals_to_Free @{thm rat_mult_poly_r}),
1.255 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
1.256
1.257 - Rule.Thm ("real_divide_divide1_mg", TermC.num_str @{thm real_divide_divide1_mg}),
1.258 + Rule.Thm ("real_divide_divide1_mg", ThmC.numerals_to_Free @{thm real_divide_divide1_mg}),
1.259 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
1.260 - Rule.Thm ("divide_divide_eq_right", TermC.num_str @{thm divide_divide_eq_right}),
1.261 + Rule.Thm ("divide_divide_eq_right", ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
1.262 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
1.263 - Rule.Thm ("divide_divide_eq_left", TermC.num_str @{thm divide_divide_eq_left}),
1.264 + Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
1.265 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
1.266 Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
1.267
1.268 - Rule.Thm ("rat_power", TermC.num_str @{thm rat_power})
1.269 + Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
1.270 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
1.271 ],
1.272 scr = Rule.EmptyScr});
1.273 @@ -818,9 +818,9 @@
1.274 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.275 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.276 rules =
1.277 - [Rule.Thm ("div_by_1", TermC.num_str @{thm div_by_1}),
1.278 + [Rule.Thm ("div_by_1", ThmC.numerals_to_Free @{thm div_by_1}),
1.279 (*"?x / 1 = ?x"*)
1.280 - Rule.Thm ("mult_1_left", TermC.num_str @{thm mult_1_left})
1.281 + Rule.Thm ("mult_1_left", ThmC.numerals_to_Free @{thm mult_1_left})
1.282 (*"1 * z = z"*)
1.283 ],
1.284 scr = Rule.EmptyScr});