equal
deleted
inserted
replaced
395 qed |
395 qed |
396 |
396 |
397 ML {* |
397 ML {* |
398 fun atomize_thm thm = |
398 fun atomize_thm thm = |
399 let |
399 let |
400 val thm' = forall_intr_vars thm |
400 val thm' = Thm.freezeT (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 @{thm Pure.equal_elim_rule1} OF [thm'', thm'] |
403 @{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 |