1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Mon Apr 13 13:27:55 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Mon Apr 13 15:31:23 2020 +0200
1.3 @@ -194,21 +194,21 @@
1.4 Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [],
1.5 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
1.6 erls = erls_ordne_alphabetisch,
1.7 - rules = [Rule.Thm ("tausche_plus",TermC.num_str @{thm tausche_plus}),
1.8 + rules = [Rule.Thm ("tausche_plus",ThmC.numerals_to_Free @{thm tausche_plus}),
1.9 (*"b kleiner a ==> (b + a) = (a + b)"*)
1.10 - Rule.Thm ("tausche_minus",TermC.num_str @{thm tausche_minus}),
1.11 + Rule.Thm ("tausche_minus",ThmC.numerals_to_Free @{thm tausche_minus}),
1.12 (*"b kleiner a ==> (b - a) = (-a + b)"*)
1.13 - Rule.Thm ("tausche_vor_plus",TermC.num_str @{thm tausche_vor_plus}),
1.14 + Rule.Thm ("tausche_vor_plus",ThmC.numerals_to_Free @{thm tausche_vor_plus}),
1.15 (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
1.16 - Rule.Thm ("tausche_vor_minus",TermC.num_str @{thm tausche_vor_minus}),
1.17 + Rule.Thm ("tausche_vor_minus",ThmC.numerals_to_Free @{thm tausche_vor_minus}),
1.18 (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
1.19 - Rule.Thm ("tausche_plus_plus",TermC.num_str @{thm tausche_plus_plus}),
1.20 + Rule.Thm ("tausche_plus_plus",ThmC.numerals_to_Free @{thm tausche_plus_plus}),
1.21 (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
1.22 - Rule.Thm ("tausche_plus_minus",TermC.num_str @{thm tausche_plus_minus}),
1.23 + Rule.Thm ("tausche_plus_minus",ThmC.numerals_to_Free @{thm tausche_plus_minus}),
1.24 (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
1.25 - Rule.Thm ("tausche_minus_plus",TermC.num_str @{thm tausche_minus_plus}),
1.26 + Rule.Thm ("tausche_minus_plus",ThmC.numerals_to_Free @{thm tausche_minus_plus}),
1.27 (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
1.28 - Rule.Thm ("tausche_minus_minus",TermC.num_str @{thm tausche_minus_minus})
1.29 + Rule.Thm ("tausche_minus_minus",ThmC.numerals_to_Free @{thm tausche_minus_minus})
1.30 (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
1.31 ], scr = Rule.EmptyScr};
1.32
1.33 @@ -219,42 +219,42 @@
1.34 [Rule.Num_Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")],
1.35 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.36 rules =
1.37 - [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1.38 + [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
1.39 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.40 - Rule.Thm ("real_num_collect_assoc_r",TermC.num_str @{thm real_num_collect_assoc_r}),
1.41 + Rule.Thm ("real_num_collect_assoc_r",ThmC.numerals_to_Free @{thm real_num_collect_assoc_r}),
1.42 (*"[| l is_const; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
1.43 - Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
1.44 + Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
1.45 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.46 - Rule.Thm ("real_one_collect_assoc_r",TermC.num_str @{thm real_one_collect_assoc_r}),
1.47 + Rule.Thm ("real_one_collect_assoc_r",ThmC.numerals_to_Free @{thm real_one_collect_assoc_r}),
1.48 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
1.49
1.50
1.51 - Rule.Thm ("subtrahiere",TermC.num_str @{thm subtrahiere}),
1.52 + Rule.Thm ("subtrahiere",ThmC.numerals_to_Free @{thm subtrahiere}),
1.53 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
1.54 - Rule.Thm ("subtrahiere_von_1",TermC.num_str @{thm subtrahiere_von_1}),
1.55 + Rule.Thm ("subtrahiere_von_1",ThmC.numerals_to_Free @{thm subtrahiere_von_1}),
1.56 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
1.57 - Rule.Thm ("subtrahiere_1",TermC.num_str @{thm subtrahiere_1}),
1.58 + Rule.Thm ("subtrahiere_1",ThmC.numerals_to_Free @{thm subtrahiere_1}),
1.59 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
1.60
1.61 - Rule.Thm ("subtrahiere_x_plus_minus",TermC.num_str @{thm subtrahiere_x_plus_minus}),
1.62 + Rule.Thm ("subtrahiere_x_plus_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_plus_minus}),
1.63 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
1.64 - Rule.Thm ("subtrahiere_x_plus1_minus",TermC.num_str @{thm subtrahiere_x_plus1_minus}),
1.65 + Rule.Thm ("subtrahiere_x_plus1_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_plus1_minus}),
1.66 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
1.67 - Rule.Thm ("subtrahiere_x_plus_minus1",TermC.num_str @{thm subtrahiere_x_plus_minus1}),
1.68 + Rule.Thm ("subtrahiere_x_plus_minus1",ThmC.numerals_to_Free @{thm subtrahiere_x_plus_minus1}),
1.69 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
1.70
1.71 - Rule.Thm ("subtrahiere_x_minus_plus",TermC.num_str @{thm subtrahiere_x_minus_plus}),
1.72 + Rule.Thm ("subtrahiere_x_minus_plus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_plus}),
1.73 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
1.74 - Rule.Thm ("subtrahiere_x_minus1_plus",TermC.num_str @{thm subtrahiere_x_minus1_plus}),
1.75 + Rule.Thm ("subtrahiere_x_minus1_plus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus1_plus}),
1.76 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
1.77 - Rule.Thm ("subtrahiere_x_minus_plus1",TermC.num_str @{thm subtrahiere_x_minus_plus1}),
1.78 + Rule.Thm ("subtrahiere_x_minus_plus1",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_plus1}),
1.79 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
1.80
1.81 - Rule.Thm ("subtrahiere_x_minus_minus",TermC.num_str @{thm subtrahiere_x_minus_minus}),
1.82 + Rule.Thm ("subtrahiere_x_minus_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_minus}),
1.83 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
1.84 - Rule.Thm ("subtrahiere_x_minus1_minus",TermC.num_str @{thm subtrahiere_x_minus1_minus}),
1.85 + Rule.Thm ("subtrahiere_x_minus1_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus1_minus}),
1.86 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
1.87 - Rule.Thm ("subtrahiere_x_minus_minus1",TermC.num_str @{thm subtrahiere_x_minus_minus1}),
1.88 + Rule.Thm ("subtrahiere_x_minus_minus1",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_minus1}),
1.89 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
1.90
1.91 Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.92 @@ -262,18 +262,18 @@
1.93
1.94 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
1.95 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
1.96 - Rule.Thm ("real_mult_2_assoc_r",TermC.num_str @{thm real_mult_2_assoc_r}),
1.97 + Rule.Thm ("real_mult_2_assoc_r",ThmC.numerals_to_Free @{thm real_mult_2_assoc_r}),
1.98 (*"(k + z1) + z1 = k + 2 * z1"*)
1.99 - Rule.Thm ("sym_real_mult_2",TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
1.100 + Rule.Thm ("sym_real_mult_2",ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
1.101 (*"z1 + z1 = 2 * z1"*)
1.102
1.103 - Rule.Thm ("addiere_vor_minus",TermC.num_str @{thm addiere_vor_minus}),
1.104 + Rule.Thm ("addiere_vor_minus",ThmC.numerals_to_Free @{thm addiere_vor_minus}),
1.105 (*"[| l is_const; m is_const |] ==> -(l * v) + m * v = (-l + m) *v"*)
1.106 - Rule.Thm ("addiere_eins_vor_minus",TermC.num_str @{thm addiere_eins_vor_minus}),
1.107 + Rule.Thm ("addiere_eins_vor_minus",ThmC.numerals_to_Free @{thm addiere_eins_vor_minus}),
1.108 (*"[| m is_const |] ==> - v + m * v = (-1 + m) * v"*)
1.109 - Rule.Thm ("subtrahiere_vor_minus",TermC.num_str @{thm subtrahiere_vor_minus}),
1.110 + Rule.Thm ("subtrahiere_vor_minus",ThmC.numerals_to_Free @{thm subtrahiere_vor_minus}),
1.111 (*"[| l is_const; m is_const |] ==> -(l * v) - m * v = (-l - m) *v"*)
1.112 - Rule.Thm ("subtrahiere_eins_vor_minus",TermC.num_str @{thm subtrahiere_eins_vor_minus})
1.113 + Rule.Thm ("subtrahiere_eins_vor_minus",ThmC.numerals_to_Free @{thm subtrahiere_eins_vor_minus})
1.114 (*"[| m is_const |] ==> - v - m * v = (-1 - m) * v"*)
1.115
1.116 ], scr = Rule.EmptyScr};
1.117 @@ -283,29 +283,29 @@
1.118 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
1.119 erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty
1.120 [Rule.Num_Calc ("PolyMinus.kleiner", eval_kleiner "")],
1.121 - rules = [Rule.Thm ("vorzeichen_minus_weg1",TermC.num_str @{thm vorzeichen_minus_weg1}),
1.122 + rules = [Rule.Thm ("vorzeichen_minus_weg1",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg1}),
1.123 (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
1.124 - Rule.Thm ("vorzeichen_minus_weg2",TermC.num_str @{thm vorzeichen_minus_weg2}),
1.125 + Rule.Thm ("vorzeichen_minus_weg2",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg2}),
1.126 (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
1.127 - Rule.Thm ("vorzeichen_minus_weg3",TermC.num_str @{thm vorzeichen_minus_weg3}),
1.128 + Rule.Thm ("vorzeichen_minus_weg3",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg3}),
1.129 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
1.130 - Rule.Thm ("vorzeichen_minus_weg4",TermC.num_str @{thm vorzeichen_minus_weg4}),
1.131 + Rule.Thm ("vorzeichen_minus_weg4",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg4}),
1.132 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
1.133
1.134 Rule.Num_Calc ("Groups.times_class.times", (**)eval_binop "#mult_"),
1.135
1.136 - Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1.137 + Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
1.138 (*"0 * z = 0"*)
1.139 - Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1.140 + Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
1.141 (*"1 * z = z"*)
1.142 - Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
1.143 + Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
1.144 (*"0 + z = z"*)
1.145 - Rule.Thm ("null_minus",TermC.num_str @{thm null_minus}),
1.146 + Rule.Thm ("null_minus",ThmC.numerals_to_Free @{thm null_minus}),
1.147 (*"0 - a = -a"*)
1.148 - Rule.Thm ("vor_minus_mal",TermC.num_str @{thm vor_minus_mal})
1.149 + Rule.Thm ("vor_minus_mal",ThmC.numerals_to_Free @{thm vor_minus_mal})
1.150 (*"- a * b = (-a) * b"*)
1.151
1.152 - (*Rule.Thm ("",TermC.num_str @{}),*)
1.153 + (*Rule.Thm ("",ThmC.numerals_to_Free @{}),*)
1.154 (**)
1.155 ], scr = Rule.EmptyScr} (*end verschoenere*);
1.156
1.157 @@ -313,30 +313,30 @@
1.158 Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [],
1.159 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
1.160 rules = [Rule.Thm ("sym_add_assoc",
1.161 - TermC.num_str (@{thm add.assoc} RS @{thm sym})),
1.162 + ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
1.163 (*"a + (b + c) = (a + b) + c"*)
1.164 - Rule.Thm ("klammer_plus_minus",TermC.num_str @{thm klammer_plus_minus}),
1.165 + Rule.Thm ("klammer_plus_minus",ThmC.numerals_to_Free @{thm klammer_plus_minus}),
1.166 (*"a + (b - c) = (a + b) - c"*)
1.167 - Rule.Thm ("klammer_minus_plus",TermC.num_str @{thm klammer_minus_plus}),
1.168 + Rule.Thm ("klammer_minus_plus",ThmC.numerals_to_Free @{thm klammer_minus_plus}),
1.169 (*"a - (b + c) = (a - b) - c"*)
1.170 - Rule.Thm ("klammer_minus_minus",TermC.num_str @{thm klammer_minus_minus})
1.171 + Rule.Thm ("klammer_minus_minus",ThmC.numerals_to_Free @{thm klammer_minus_minus})
1.172 (*"a - (b - c) = (a - b) + c"*)
1.173 ], scr = Rule.EmptyScr};
1.174
1.175 val klammern_ausmultiplizieren =
1.176 Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [],
1.177 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty,
1.178 - rules = [Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
1.179 + rules = [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
1.180 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.181 - Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
1.182 + Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
1.183 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1.184
1.185 - Rule.Thm ("klammer_mult_minus",TermC.num_str @{thm klammer_mult_minus}),
1.186 + Rule.Thm ("klammer_mult_minus",ThmC.numerals_to_Free @{thm klammer_mult_minus}),
1.187 (*"a * (b - c) = a * b - a * c"*)
1.188 - Rule.Thm ("klammer_minus_mult",TermC.num_str @{thm klammer_minus_mult})
1.189 + Rule.Thm ("klammer_minus_mult",ThmC.numerals_to_Free @{thm klammer_minus_mult})
1.190 (*"(b - c) * a = b * a - c * a"*)
1.191
1.192 - (*Rule.Thm ("",TermC.num_str @{}),
1.193 + (*Rule.Thm ("",ThmC.numerals_to_Free @{}),
1.194 (*""*)*)
1.195 ], scr = Rule.EmptyScr};
1.196
1.197 @@ -347,16 +347,16 @@
1.198 [Rule.Num_Calc ("PolyMinus.kleiner", eval_kleiner ""),
1.199 Rule.Num_Calc ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "")
1.200 ],
1.201 - rules = [Rule.Thm ("tausche_mal",TermC.num_str @{thm tausche_mal}),
1.202 + rules = [Rule.Thm ("tausche_mal",ThmC.numerals_to_Free @{thm tausche_mal}),
1.203 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
1.204 - Rule.Thm ("tausche_vor_mal",TermC.num_str @{thm tausche_vor_mal}),
1.205 + Rule.Thm ("tausche_vor_mal",ThmC.numerals_to_Free @{thm tausche_vor_mal}),
1.206 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
1.207 - Rule.Thm ("tausche_mal_mal",TermC.num_str @{thm tausche_mal_mal}),
1.208 + Rule.Thm ("tausche_mal_mal",ThmC.numerals_to_Free @{thm tausche_mal_mal}),
1.209 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
1.210 - Rule.Thm ("x_quadrat",TermC.num_str @{thm x_quadrat})
1.211 + Rule.Thm ("x_quadrat",ThmC.numerals_to_Free @{thm x_quadrat})
1.212 (*"(x * a) * a = x * a ^^^ 2"*)
1.213
1.214 - (*Rule.Thm ("",TermC.num_str @{}),
1.215 + (*Rule.Thm ("",ThmC.numerals_to_Free @{}),
1.216 (*""*)*)
1.217 ], scr = Rule.EmptyScr};
1.218
1.219 @@ -410,13 +410,13 @@
1.220 Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty
1.221 [Rule.Num_Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
1.222 Rule.Num_Calc ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
1.223 - Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
1.224 + Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
1.225 (*"(?a | True) = True"*)
1.226 - Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
1.227 + Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
1.228 (*"(?a | False) = ?a"*)
1.229 - Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.230 + Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1.231 (*"(~ True) = False"*)
1.232 - Rule.Thm ("not_false",TermC.num_str @{thm not_false})
1.233 + Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
1.234 (*"(~ False) = True"*)],
1.235 SOME "Vereinfache t_t", [["simplification","for_polynomials","with_minus"]])),
1.236 (Specify.prep_pbt thy "pbl_vereinf_poly_klammer" [] Celem.e_pblID
1.237 @@ -431,13 +431,13 @@
1.238 Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty
1.239 [Rule.Num_Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
1.240 Rule.Num_Calc ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
1.241 - Rule.Thm ("or_true", TermC.num_str @{thm or_true}),
1.242 + Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
1.243 (*"(?a | True) = True"*)
1.244 - Rule.Thm ("or_false", TermC.num_str @{thm or_false}),
1.245 + Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
1.246 (*"(?a | False) = ?a"*)
1.247 - Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.248 + Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1.249 (*"(~ True) = False"*)
1.250 - Rule.Thm ("not_false",TermC.num_str @{thm not_false})
1.251 + Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
1.252 (*"(~ False) = True"*)],
1.253 SOME "Vereinfache t_t",
1.254 [["simplification","for_polynomials","with_parentheses"]])),
1.255 @@ -493,13 +493,13 @@
1.256 prls = Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty
1.257 [Rule.Num_Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
1.258 Rule.Num_Calc ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
1.259 - Rule.Thm ("and_true",TermC.num_str @{thm and_true}),
1.260 + Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
1.261 (*"(?a & True) = ?a"*)
1.262 - Rule.Thm ("and_false",TermC.num_str @{thm and_false}),
1.263 + Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
1.264 (*"(?a & False) = False"*)
1.265 - Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.266 + Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1.267 (*"(~ True) = False"*)
1.268 - Rule.Thm ("not_false",TermC.num_str @{thm not_false})
1.269 + Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
1.270 (*"(~ False) = True"*)],
1.271 crls = Rule_Set.empty, errpats = [], nrls = rls_p_33},
1.272 @{thm simplify.simps})]