src/HOL/Extraction.thy
changeset 18456 8cc35e95450a
parent 17203 29b2563f5c11
child 18511 beed2bc052a3
equal deleted inserted replaced
18455:b293c1087f1d 18456:8cc35e95450a
    47       ProofRewriteRules.elim_vars (curry Const "arbitrary"))]
    47       ProofRewriteRules.elim_vars (curry Const "arbitrary"))]
    48 end
    48 end
    49 *}
    49 *}
    50 
    50 
    51 lemmas [extraction_expand] =
    51 lemmas [extraction_expand] =
    52   atomize_eq atomize_all atomize_imp
    52   atomize_eq atomize_all atomize_imp atomize_conj
    53   allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
    53   allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
    54   notE' impE' impE iffE imp_cong simp_thms
    54   notE' impE' impE iffE imp_cong simp_thms
    55   induct_forall_eq induct_implies_eq induct_equal_eq
    55   induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
    56   induct_forall_def induct_implies_def induct_impliesI
    56   induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    57   induct_atomize induct_rulify1 induct_rulify2
    57   induct_atomize induct_atomize_old induct_rulify induct_rulify_fallback
    58 
    58 
    59 datatype sumbool = Left | Right
    59 datatype sumbool = Left | Right
    60 
    60 
    61 subsection {* Type of extracted program *}
    61 subsection {* Type of extracted program *}
    62 
    62