equal
deleted
inserted
replaced
1702 @{ML_response_fake [display,gray] |
1702 @{ML_response_fake [display,gray] |
1703 "let |
1703 "let |
1704 val thm = @{thm foo_test1} |
1704 val thm = @{thm foo_test1} |
1705 val meta_eq = Object_Logic.atomize (cprop_of thm) |
1705 val meta_eq = Object_Logic.atomize (cprop_of thm) |
1706 in |
1706 in |
1707 MetaSimplifier.rewrite_rule [meta_eq] thm |
1707 Raw_Simplifier.rewrite_rule [meta_eq] thm |
1708 end" |
1708 end" |
1709 "?A \<longrightarrow> ?B \<longrightarrow> ?C"} |
1709 "?A \<longrightarrow> ?B \<longrightarrow> ?C"} |
1710 |
1710 |
1711 In this code the function @{ML atomize in Object_Logic} produces |
1711 In this code the function @{ML atomize in Object_Logic} produces |
1712 a meta-equation between the given theorem and the theorem transformed |
1712 a meta-equation between the given theorem and the theorem transformed |
1726 ML{*fun atomize_thm thm = |
1726 ML{*fun atomize_thm thm = |
1727 let |
1727 let |
1728 val thm' = forall_intr_vars thm |
1728 val thm' = forall_intr_vars thm |
1729 val thm'' = Object_Logic.atomize (cprop_of thm') |
1729 val thm'' = Object_Logic.atomize (cprop_of thm') |
1730 in |
1730 in |
1731 MetaSimplifier.rewrite_rule [thm''] thm' |
1731 Raw_Simplifier.rewrite_rule [thm''] thm' |
1732 end*} |
1732 end*} |
1733 |
1733 |
1734 text {* |
1734 text {* |
1735 This function produces for the theorem @{thm [source] list.induct} |
1735 This function produces for the theorem @{thm [source] list.induct} |
1736 |
1736 |