equal
deleted
inserted
replaced
15 setup \<open> |
15 setup \<open> |
16 Extraction.add_types |
16 Extraction.add_types |
17 [("bool", ([], NONE))] #> |
17 [("bool", ([], NONE))] #> |
18 Extraction.set_preprocessor (fn thy => |
18 Extraction.set_preprocessor (fn thy => |
19 Proofterm.rewrite_proof_notypes |
19 Proofterm.rewrite_proof_notypes |
20 ([], RewriteHOLProof.elim_cong :: ProofRewriteRules.rprocs true) o |
20 ([], Rewrite_HOL_Proof.elim_cong :: Proof_Rewrite_Rules.rprocs true) o |
21 Proofterm.rewrite_proof thy |
21 Proofterm.rewrite_proof thy |
22 (RewriteHOLProof.rews, |
22 (Rewrite_HOL_Proof.rews, |
23 ProofRewriteRules.rprocs true @ [ProofRewriteRules.expand_of_class thy]) o |
23 Proof_Rewrite_Rules.rprocs true @ [Proof_Rewrite_Rules.expand_of_class thy]) o |
24 ProofRewriteRules.elim_vars (curry Const \<^const_name>\<open>default\<close>)) |
24 Proof_Rewrite_Rules.elim_vars (curry Const \<^const_name>\<open>default\<close>)) |
25 \<close> |
25 \<close> |
26 |
26 |
27 lemmas [extraction_expand] = |
27 lemmas [extraction_expand] = |
28 meta_spec atomize_eq atomize_all atomize_imp atomize_conj |
28 meta_spec atomize_eq atomize_all atomize_imp atomize_conj |
29 allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |
29 allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2 |