equal
deleted
inserted
replaced
215 |
215 |
216 fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm) |
216 fun sym_Thm (Thm (thmID, thm)) = Thm (sym_thmID thmID, sym_thm thm) |
217 | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls) |
217 | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls) |
218 | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r)); |
218 | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r)); |
219 (* |
219 (* |
220 val th = Thm ("real_one_collect",num_str real_one_collect); |
220 val th = Thm ("real_one_collect",num_str @{real_one_collect); |
221 sym_Thm th; |
221 sym_Thm th; |
222 val th = |
222 val th = |
223 Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n") |
223 Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n") |
224 : rule |
224 : rule |
225 ML> val it = |
225 ML> val it = |