1.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Aug 31 15:36:57 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Aug 31 16:00:13 2010 +0200
1.3 @@ -209,17 +209,17 @@
1.4 Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
1.5 erls = e_rls, srls = Erls,
1.6 calc = [],
1.7 - rules = [Thm ("refl",num_str refl),
1.8 + rules = [Thm ("refl",num_str @{refl),
1.9 Thm ("real_le_refl",num_str @{thm real_le_refl}),
1.10 - Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
1.11 - Thm ("not_true",num_str not_true),
1.12 - Thm ("not_false",num_str not_false),
1.13 + Thm ("radd_left_cancel_le",num_str @{radd_left_cancel_le),
1.14 + Thm ("not_true",num_str @{not_true),
1.15 + Thm ("not_false",num_str @{not_false),
1.16 Thm ("and_true",and_true),
1.17 Thm ("and_false",and_false),
1.18 Thm ("or_true",or_true),
1.19 Thm ("or_false",or_false),
1.20 - Thm ("and_commute",num_str and_commute),
1.21 - Thm ("or_commute",num_str or_commute),
1.22 + Thm ("and_commute",num_str @{and_commute),
1.23 + Thm ("or_commute",num_str @{or_commute),
1.24
1.25 Calc ("Atools.is'_const",eval_const "#is_const_"),
1.26 Calc ("Tools.matches",eval_matches ""),
1.27 @@ -243,24 +243,24 @@
1.28 rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),
1.29 erls=testerls,srls = e_rls,
1.30 calc=[],
1.31 - rules = [Thm ("refl",num_str refl),
1.32 + rules = [Thm ("refl",num_str @{refl),
1.33 Thm ("real_le_refl",num_str @{thm real_le_refl}),
1.34 - Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
1.35 - Thm ("not_true",num_str not_true),
1.36 - Thm ("not_false",num_str not_false),
1.37 + Thm ("radd_left_cancel_le",num_str @{radd_left_cancel_le),
1.38 + Thm ("not_true",num_str @{not_true),
1.39 + Thm ("not_false",num_str @{not_false),
1.40 Thm ("and_true",and_true),
1.41 Thm ("and_false",and_false),
1.42 Thm ("or_true",or_true),
1.43 Thm ("or_false",or_false),
1.44 - Thm ("and_commute",num_str and_commute),
1.45 - Thm ("or_commute",num_str or_commute),
1.46 + Thm ("and_commute",num_str @{and_commute),
1.47 + Thm ("or_commute",num_str @{or_commute),
1.48
1.49 - Thm ("real_diff_minus",num_str real_diff_minus),
1.50 + Thm ("real_diff_minus",num_str @{real_diff_minus),
1.51
1.52 - Thm ("root_ge0",num_str root_ge0),
1.53 - Thm ("root_add_ge0",num_str root_add_ge0),
1.54 - Thm ("root_ge0_1",num_str root_ge0_1),
1.55 - Thm ("root_ge0_2",num_str root_ge0_2),
1.56 + Thm ("root_ge0",num_str @{root_ge0),
1.57 + Thm ("root_add_ge0",num_str @{root_add_ge0),
1.58 + Thm ("root_ge0_1",num_str @{root_ge0_1),
1.59 + Thm ("root_ge0_2",num_str @{root_ge0_2),
1.60
1.61 Calc ("Atools.is'_const",eval_const "#is_const_"),
1.62 Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_"),
1.63 @@ -293,8 +293,8 @@
1.64 rew_ord = ("e_rew_ord",e_rew_ord),
1.65 erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
1.66 rules =
1.67 - [Thm ("sym_radd_assoc",num_str (radd_assoc RS sym)),
1.68 - Thm ("sym_rmult_assoc",num_str (rmult_assoc RS sym))],
1.69 + [Thm ("sym_radd_assoc",num_str @{(radd_assoc RS sym)),
1.70 + Thm ("sym_rmult_assoc",num_str @{(rmult_assoc RS sym))],
1.71 scr = Script ((term_of o the o (parse thy))
1.72 "empty_script")
1.73 }:rls;
1.74 @@ -313,11 +313,11 @@
1.75 "empty_script")
1.76 }:rls;
1.77
1.78 -(*todo: replace by Rewrite("rnorm_equation_add",num_str rnorm_equation_add)*)
1.79 +(*todo: replace by Rewrite("rnorm_equation_add",num_str @{rnorm_equation_add)*)
1.80 val norm_equation =
1.81 Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.82 erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
1.83 - rules = [Thm ("rnorm_equation_add",num_str rnorm_equation_add)
1.84 + rules = [Thm ("rnorm_equation_add",num_str @{rnorm_equation_add)
1.85 ],
1.86 scr = Script ((term_of o the o (parse thy))
1.87 "empty_script")
1.88 @@ -381,22 +381,22 @@
1.89 calc=[(*since 040209 filled by prep_rls*)],
1.90 (*asm_thm = [],*)
1.91 rules = [
1.92 - Thm ("real_diff_minus",num_str real_diff_minus),
1.93 - Thm ("radd_mult_distrib2",num_str radd_mult_distrib2),
1.94 - Thm ("rdistr_right_assoc",num_str rdistr_right_assoc),
1.95 - Thm ("rdistr_right_assoc_p",num_str rdistr_right_assoc_p),
1.96 - Thm ("rdistr_div_right",num_str rdistr_div_right),
1.97 - Thm ("rbinom_power_2",num_str rbinom_power_2),
1.98 + Thm ("real_diff_minus",num_str @{real_diff_minus),
1.99 + Thm ("radd_mult_distrib2",num_str @{radd_mult_distrib2),
1.100 + Thm ("rdistr_right_assoc",num_str @{rdistr_right_assoc),
1.101 + Thm ("rdistr_right_assoc_p",num_str @{rdistr_right_assoc_p),
1.102 + Thm ("rdistr_div_right",num_str @{rdistr_div_right),
1.103 + Thm ("rbinom_power_2",num_str @{rbinom_power_2),
1.104
1.105 - Thm ("radd_commute",num_str radd_commute),
1.106 - Thm ("radd_left_commute",num_str radd_left_commute),
1.107 - Thm ("radd_assoc",num_str radd_assoc),
1.108 - Thm ("rmult_commute",num_str rmult_commute),
1.109 - Thm ("rmult_left_commute",num_str rmult_left_commute),
1.110 - Thm ("rmult_assoc",num_str rmult_assoc),
1.111 + Thm ("radd_commute",num_str @{radd_commute),
1.112 + Thm ("radd_left_commute",num_str @{radd_left_commute),
1.113 + Thm ("radd_assoc",num_str @{radd_assoc),
1.114 + Thm ("rmult_commute",num_str @{rmult_commute),
1.115 + Thm ("rmult_left_commute",num_str @{rmult_left_commute),
1.116 + Thm ("rmult_assoc",num_str @{rmult_assoc),
1.117
1.118 - Thm ("radd_real_const_eq",num_str radd_real_const_eq),
1.119 - Thm ("radd_real_const",num_str radd_real_const),
1.120 + Thm ("radd_real_const_eq",num_str @{radd_real_const_eq),
1.121 + Thm ("radd_real_const",num_str @{radd_real_const),
1.122 (* these 2 rules are invers to distr_div_right wrt. termination.
1.123 thus they MUST be done IMMEDIATELY before calc *)
1.124 Calc ("op +", eval_binop "#add_"),
1.125 @@ -404,27 +404,27 @@
1.126 Calc ("HOL.divide", eval_cancel "#divide_"),
1.127 Calc ("Atools.pow", eval_binop "#power_"),
1.128
1.129 - Thm ("rcollect_right",num_str rcollect_right),
1.130 - Thm ("rcollect_one_left",num_str rcollect_one_left),
1.131 - Thm ("rcollect_one_left_assoc",num_str rcollect_one_left_assoc),
1.132 - Thm ("rcollect_one_left_assoc_p",num_str rcollect_one_left_assoc_p),
1.133 + Thm ("rcollect_right",num_str @{rcollect_right),
1.134 + Thm ("rcollect_one_left",num_str @{rcollect_one_left),
1.135 + Thm ("rcollect_one_left_assoc",num_str @{rcollect_one_left_assoc),
1.136 + Thm ("rcollect_one_left_assoc_p",num_str @{rcollect_one_left_assoc_p),
1.137
1.138 - Thm ("rshift_nominator",num_str rshift_nominator),
1.139 - Thm ("rcancel_den",num_str rcancel_den),
1.140 - Thm ("rroot_square_inv",num_str rroot_square_inv),
1.141 - Thm ("rroot_times_root",num_str rroot_times_root),
1.142 - Thm ("rroot_times_root_assoc_p",num_str rroot_times_root_assoc_p),
1.143 - Thm ("rsqare",num_str rsqare),
1.144 - Thm ("power_1",num_str power_1),
1.145 - Thm ("rtwo_of_the_same",num_str rtwo_of_the_same),
1.146 - Thm ("rtwo_of_the_same_assoc_p",num_str rtwo_of_the_same_assoc_p),
1.147 + Thm ("rshift_nominator",num_str @{rshift_nominator),
1.148 + Thm ("rcancel_den",num_str @{rcancel_den),
1.149 + Thm ("rroot_square_inv",num_str @{rroot_square_inv),
1.150 + Thm ("rroot_times_root",num_str @{rroot_times_root),
1.151 + Thm ("rroot_times_root_assoc_p",num_str @{rroot_times_root_assoc_p),
1.152 + Thm ("rsqare",num_str @{rsqare),
1.153 + Thm ("power_1",num_str @{power_1),
1.154 + Thm ("rtwo_of_the_same",num_str @{rtwo_of_the_same),
1.155 + Thm ("rtwo_of_the_same_assoc_p",num_str @{rtwo_of_the_same_assoc_p),
1.156
1.157 - Thm ("rmult_1",num_str rmult_1),
1.158 - Thm ("rmult_1_right",num_str rmult_1_right),
1.159 - Thm ("rmult_0",num_str rmult_0),
1.160 - Thm ("rmult_0_right",num_str rmult_0_right),
1.161 - Thm ("radd_0",num_str radd_0),
1.162 - Thm ("radd_0_right",num_str radd_0_right)
1.163 + Thm ("rmult_1",num_str @{rmult_1),
1.164 + Thm ("rmult_1_right",num_str @{rmult_1_right),
1.165 + Thm ("rmult_0",num_str @{rmult_0),
1.166 + Thm ("rmult_0_right",num_str @{rmult_0_right),
1.167 + Thm ("radd_0",num_str @{radd_0),
1.168 + Thm ("radd_0_right",num_str @{radd_0_right)
1.169 ],
1.170 scr = Script ((term_of o the o (parse thy)) "empty_script")
1.171 (*since 040209 filled by prep_rls: STest_simplify*)
1.172 @@ -442,12 +442,12 @@
1.173 val isolate_root =
1.174 Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.175 erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
1.176 - rules = [Thm ("rroot_to_lhs",num_str rroot_to_lhs),
1.177 - Thm ("rroot_to_lhs_mult",num_str rroot_to_lhs_mult),
1.178 - Thm ("rroot_to_lhs_add_mult",num_str rroot_to_lhs_add_mult),
1.179 - Thm ("risolate_root_add",num_str risolate_root_add),
1.180 - Thm ("risolate_root_mult",num_str risolate_root_mult),
1.181 - Thm ("risolate_root_div",num_str risolate_root_div) ],
1.182 + rules = [Thm ("rroot_to_lhs",num_str @{rroot_to_lhs),
1.183 + Thm ("rroot_to_lhs_mult",num_str @{rroot_to_lhs_mult),
1.184 + Thm ("rroot_to_lhs_add_mult",num_str @{rroot_to_lhs_add_mult),
1.185 + Thm ("risolate_root_add",num_str @{risolate_root_add),
1.186 + Thm ("risolate_root_mult",num_str @{risolate_root_mult),
1.187 + Thm ("risolate_root_div",num_str @{risolate_root_div) ],
1.188 scr = Script ((term_of o the o (parse thy))
1.189 "empty_script")
1.190 }:rls;
1.191 @@ -457,12 +457,12 @@
1.192 Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
1.193 erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
1.194 rules =
1.195 - [Thm ("risolate_bdv_add",num_str risolate_bdv_add),
1.196 - Thm ("risolate_bdv_mult_add",num_str risolate_bdv_mult_add),
1.197 - Thm ("risolate_bdv_mult",num_str risolate_bdv_mult),
1.198 - Thm ("mult_square",num_str mult_square),
1.199 - Thm ("constant_square",num_str constant_square),
1.200 - Thm ("constant_mult_square",num_str constant_mult_square)
1.201 + [Thm ("risolate_bdv_add",num_str @{risolate_bdv_add),
1.202 + Thm ("risolate_bdv_mult_add",num_str @{risolate_bdv_mult_add),
1.203 + Thm ("risolate_bdv_mult",num_str @{risolate_bdv_mult),
1.204 + Thm ("mult_square",num_str @{mult_square),
1.205 + Thm ("constant_square",num_str @{constant_square),
1.206 + Thm ("constant_mult_square",num_str @{constant_mult_square)
1.207 ],
1.208 scr = Script ((term_of o the o (parse thy))
1.209 "empty_script")
1.210 @@ -1261,7 +1261,7 @@
1.211 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.212 ],
1.213 (*asm_thm = [],*)
1.214 - rules = [Thm ("real_diff_minus",num_str real_diff_minus),
1.215 + rules = [Thm ("real_diff_minus",num_str @{real_diff_minus),
1.216 (*"a - b = a + (-1) * b"*)
1.217 Thm ("left_distrib" ,num_str @{thm left_distrib}),
1.218 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1.219 @@ -1279,11 +1279,11 @@
1.220 (*"0 + z = z"*)
1.221
1.222 (*AC-rewriting*)
1.223 - Thm ("real_mult_commute",num_str real_mult_commute),
1.224 + Thm ("real_mult_commute",num_str @{real_mult_commute),
1.225 (* z * w = w * z *)
1.226 - Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1.227 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute),
1.228 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1.229 - Thm ("real_mult_assoc",num_str real_mult_assoc),
1.230 + Thm ("real_mult_assoc",num_str @{real_mult_assoc),
1.231 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1.232 Thm ("add_commute",num_str @{thm add_commute}),
1.233 (*z + w = w + z*)
1.234 @@ -1292,23 +1292,23 @@
1.235 Thm ("add_assoc",num_str @{thm add_assoc}),
1.236 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1.237
1.238 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.239 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
1.240 (*"r1 * r1 = r1 ^^^ 2"*)
1.241 - Thm ("realpow_plus_1",num_str realpow_plus_1),
1.242 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
1.243 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.244 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.245 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
1.246 (*"z1 + z1 = 2 * z1"*)
1.247 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.248 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
1.249 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.250
1.251 - Thm ("real_num_collect",num_str real_num_collect),
1.252 + Thm ("real_num_collect",num_str @{real_num_collect),
1.253 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1.254 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.255 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
1.256 (*"[| l is_const; m is_const |] ==>
1.257 l * n + (m * n + k) = (l + m) * n + k"*)
1.258 - Thm ("real_one_collect",num_str real_one_collect),
1.259 + Thm ("real_one_collect",num_str @{real_one_collect),
1.260 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.261 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.262 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
1.263 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.264
1.265 Calc ("op +", eval_binop "#add_"),
1.266 @@ -1363,32 +1363,32 @@
1.267 ("POWER", ("Atools.pow", eval_binop "#power_"))
1.268 ],
1.269 (*asm_thm = [],*)
1.270 - rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
1.271 + rules = [Thm ("real_plus_binom_pow2" ,num_str @{real_plus_binom_pow2),
1.272 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1.273 - Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
1.274 + Thm ("real_plus_binom_times" ,num_str @{real_plus_binom_times),
1.275 (*"(a + b)*(a + b) = ...*)
1.276 - Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
1.277 + Thm ("real_minus_binom_pow2" ,num_str @{real_minus_binom_pow2),
1.278 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1.279 - Thm ("real_minus_binom_times",num_str real_minus_binom_times),
1.280 + Thm ("real_minus_binom_times",num_str @{real_minus_binom_times),
1.281 (*"(a - b)*(a - b) = ...*)
1.282 - Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
1.283 + Thm ("real_plus_minus_binom1",num_str @{real_plus_minus_binom1),
1.284 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1.285 - Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
1.286 + Thm ("real_plus_minus_binom2",num_str @{real_plus_minus_binom2),
1.287 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1.288 (*RL 020915*)
1.289 - Thm ("real_pp_binom_times",num_str real_pp_binom_times),
1.290 + Thm ("real_pp_binom_times",num_str @{real_pp_binom_times),
1.291 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1.292 - Thm ("real_pm_binom_times",num_str real_pm_binom_times),
1.293 + Thm ("real_pm_binom_times",num_str @{real_pm_binom_times),
1.294 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1.295 - Thm ("real_mp_binom_times",num_str real_mp_binom_times),
1.296 + Thm ("real_mp_binom_times",num_str @{real_mp_binom_times),
1.297 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
1.298 - Thm ("real_mm_binom_times",num_str real_mm_binom_times),
1.299 + Thm ("real_mm_binom_times",num_str @{real_mm_binom_times),
1.300 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
1.301 - Thm ("realpow_multI",num_str realpow_multI),
1.302 + Thm ("realpow_multI",num_str @{realpow_multI),
1.303 (*(a*b)^^^n = a^^^n * b^^^n*)
1.304 - Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
1.305 + Thm ("real_plus_binom_pow3",num_str @{real_plus_binom_pow3),
1.306 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1.307 - Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3),
1.308 + Thm ("real_minus_binom_pow3",num_str @{real_minus_binom_pow3),
1.309 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1.310
1.311
1.312 @@ -1410,30 +1410,30 @@
1.313 Calc ("op *", eval_binop "#mult_"),
1.314 Calc ("Atools.pow", eval_binop "#power_"),
1.315 (*
1.316 - Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
1.317 - Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
1.318 - Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
1.319 + Thm ("real_mult_commute",num_str @{real_mult_commute), (*AC-rewriting*)
1.320 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute), (**)
1.321 + Thm ("real_mult_assoc",num_str @{real_mult_assoc), (**)
1.322 Thm ("add_commute",num_str @{thm add_commute}), (**)
1.323 Thm ("add_left_commute",num_str @{thm add_left_commute}), (**)
1.324 Thm ("add_assoc",num_str @{thm add_assoc}), (**)
1.325 *)
1.326
1.327 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
1.328 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
1.329 (*"r1 * r1 = r1 ^^^ 2"*)
1.330 - Thm ("realpow_plus_1",num_str realpow_plus_1),
1.331 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
1.332 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1.333 - (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
1.334 + (*Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
1.335 (*"z1 + z1 = 2 * z1"*)*)
1.336 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
1.337 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
1.338 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1.339
1.340 - Thm ("real_num_collect",num_str real_num_collect),
1.341 + Thm ("real_num_collect",num_str @{real_num_collect),
1.342 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1.343 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
1.344 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
1.345 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1.346 - Thm ("real_one_collect",num_str real_one_collect),
1.347 + Thm ("real_one_collect",num_str @{real_one_collect),
1.348 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1.349 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
1.350 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
1.351 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1.352
1.353 Calc ("op +", eval_binop "#add_"),