equal
deleted
inserted
replaced
353 fun atomize_thm thm = |
353 fun atomize_thm thm = |
354 let |
354 let |
355 val thm' = forall_intr_vars thm |
355 val thm' = forall_intr_vars thm |
356 val thm'' = ObjectLogic.atomize (cprop_of thm') |
356 val thm'' = ObjectLogic.atomize (cprop_of thm') |
357 in |
357 in |
358 Thm.freezeT (Simplifier.rewrite_rule [thm''] thm') |
358 Thm.freezeT @{thm Pure.equal_elim_rule1} OF [thm'', thm'] |
359 end |
359 end |
360 *} |
360 *} |
361 |
361 |
362 ML {* atomize_thm @{thm list.induct} *} |
362 ML {* atomize_thm @{thm list.induct} *} |
363 |
363 |