equal
deleted
inserted
replaced
398 fun atomize_thm thm = |
398 fun atomize_thm thm = |
399 let |
399 let |
400 val thm' = forall_intr_vars thm |
400 val thm' = forall_intr_vars thm |
401 val thm'' = ObjectLogic.atomize (cprop_of thm') |
401 val thm'' = ObjectLogic.atomize (cprop_of thm') |
402 in |
402 in |
403 Thm.freezeT (Simplifier.rewrite_rule [thm''] thm') |
403 Thm.freezeT @{thm Pure.equal_elim_rule1} OF [thm'', thm'] |
404 end |
404 end |
405 *} |
405 *} |
406 |
406 |
407 ML {* atomize_thm @{thm list.induct} *} |
407 ML {* atomize_thm @{thm list.induct} *} |
408 |
408 |