src/HOL/Extraction.thy
changeset 18456 8cc35e95450a
parent 17203 29b2563f5c11
child 18511 beed2bc052a3
     1.1 --- a/src/HOL/Extraction.thy	Wed Dec 21 17:00:57 2005 +0100
     1.2 +++ b/src/HOL/Extraction.thy	Thu Dec 22 00:28:34 2005 +0100
     1.3 @@ -49,12 +49,12 @@
     1.4  *}
     1.5  
     1.6  lemmas [extraction_expand] =
     1.7 -  atomize_eq atomize_all atomize_imp
     1.8 +  atomize_eq atomize_all atomize_imp atomize_conj
     1.9    allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
    1.10    notE' impE' impE iffE imp_cong simp_thms
    1.11 -  induct_forall_eq induct_implies_eq induct_equal_eq
    1.12 -  induct_forall_def induct_implies_def induct_impliesI
    1.13 -  induct_atomize induct_rulify1 induct_rulify2
    1.14 +  induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
    1.15 +  induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.16 +  induct_atomize induct_atomize_old induct_rulify induct_rulify_fallback
    1.17  
    1.18  datatype sumbool = Left | Right
    1.19