src/HOL/Extraction.thy
changeset 20941 beedcae49096
parent 18708 4b3dadb4fe33
child 22281 23e0fde84cb7
     1.1 --- a/src/HOL/Extraction.thy	Tue Oct 10 10:24:24 2006 +0200
     1.2 +++ b/src/HOL/Extraction.thy	Tue Oct 10 10:34:41 2006 +0200
     1.3 @@ -51,10 +51,11 @@
     1.4  lemmas [extraction_expand] =
     1.5    atomize_eq atomize_all atomize_imp atomize_conj
     1.6    allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
     1.7 -  notE' impE' impE iffE imp_cong simp_thms
     1.8 +  notE' impE' impE iffE imp_cong simp_thms eq_True eq_False
     1.9    induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
    1.10    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    1.11    induct_atomize induct_rulify induct_rulify_fallback
    1.12 +  True_implies_equals
    1.13  
    1.14  datatype sumbool = Left | Right
    1.15