280 *) |
280 *) |
281 |
281 |
282 "-------- hard-coded val rlsthmsNOTisac -----------------"; |
282 "-------- hard-coded val rlsthmsNOTisac -----------------"; |
283 "-------- hard-coded val rlsthmsNOTisac -----------------"; |
283 "-------- hard-coded val rlsthmsNOTisac -----------------"; |
284 "-------- hardcode val rlsthmsNOTisac -------------------"; |
284 "-------- hardcode val rlsthmsNOTisac -------------------"; |
285 (*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac:*) |
285 (*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac: |
|
286 WN131121: at least ERROR Unknown fact "Real.order_refl"*) |
286 val rlsthmsNOTisac = |
287 val rlsthmsNOTisac = |
287 [("HOL.refl", (prop_of o num_str) @{thm refl}), |
288 [("HOL.refl", (prop_of o num_str) @{thm refl}), |
288 ("Fun.o_apply", (prop_of o num_str) @{thm o_apply}), |
289 ("Fun.o_apply", (prop_of o num_str) @{thm o_apply}), |
289 (*/------------these are not found in ListC.thy, because they are no axioms---\*) |
290 (*/------------these are not found in ListC.thy, because they are no axioms---\*) |
290 ("ListC.LENGTH.LENGTH_CONS", (prop_of o num_str) @{thm LENGTH_CONS}), |
291 ("ListC.LENGTH.LENGTH_CONS", (prop_of o num_str) @{thm LENGTH_CONS}), |
305 ("Rings.mult_zero_class.mult_zero_right", (prop_of o num_str) @{thm mult_zero_right}), |
306 ("Rings.mult_zero_class.mult_zero_right", (prop_of o num_str) @{thm mult_zero_right}), |
306 ("Groups.monoid_add_class.add_0_left", (prop_of o num_str) @{thm add_0_left}), |
307 ("Groups.monoid_add_class.add_0_left", (prop_of o num_str) @{thm add_0_left}), |
307 ("Groups.monoid_add_class.add_0_right", (prop_of o num_str) @{thm add_0_right}), |
308 ("Groups.monoid_add_class.add_0_right", (prop_of o num_str) @{thm add_0_right}), |
308 ("Rings.division_ring_class.divide_zero_left", (prop_of o num_str) @{thm divide_zero_left}), |
309 ("Rings.division_ring_class.divide_zero_left", (prop_of o num_str) @{thm divide_zero_left}), |
309 (*###("sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*) |
310 (*###("sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*) |
310 ("RealDef.order_refl", (prop_of o num_str) @{thm order_refl}), |
311 ("Real.order_refl", (prop_of o num_str) @{thm order_refl}), |
311 ("Groups.group_add_class.minus_minus", (prop_of o num_str) @{thm minus_minus}), |
312 ("Groups.group_add_class.minus_minus", (prop_of o num_str) @{thm minus_minus}), |
312 ("RealDef.mult_commute", (prop_of o num_str) @{thm mult_commute }), |
313 ("Real.mult_commute", (prop_of o num_str) @{thm mult_commute }), |
313 ("RealDef.mult_assoc", (prop_of o num_str) @{thm mult_assoc}), |
314 ("Real.mult_assoc", (prop_of o num_str) @{thm mult_assoc}), |
314 ("Groups.ab_semigroup_add_class.add_commute", (prop_of o num_str) @{thm add_commute}), |
315 ("Groups.ab_semigroup_add_class.add_commute", (prop_of o num_str) @{thm add_commute}), |
315 ("Groups.ab_semigroup_add_class.add_left_commute", (prop_of o num_str) @{thm add_left_commute}), |
316 ("Groups.ab_semigroup_add_class.add_left_commute", (prop_of o num_str) @{thm add_left_commute}), |
316 ("Groups.semigroup_add_class.add_assoc", (prop_of o num_str) @{thm add_assoc}), |
317 ("Groups.semigroup_add_class.add_assoc", (prop_of o num_str) @{thm add_assoc}), |
317 ("Rings.ring_class.minus_mult_left", (prop_of o num_str) @{thm minus_mult_left}), |
318 ("Rings.ring_class.minus_mult_left", (prop_of o num_str) @{thm minus_mult_left}), |
318 ("Groups.group_add_class.right_minus", (prop_of o num_str) @{thm right_minus}), |
319 ("Groups.group_add_class.right_minus", (prop_of o num_str) @{thm right_minus}), |