src/HOL/Extraction.thy
changeset 22281 23e0fde84cb7
parent 20941 beedcae49096
child 24162 8dfd5dd65d82
     1.1 --- a/src/HOL/Extraction.thy	Wed Feb 07 18:04:44 2007 +0100
     1.2 +++ b/src/HOL/Extraction.thy	Wed Feb 07 18:07:10 2007 +0100
     1.3 @@ -49,7 +49,7 @@
     1.4  *}
     1.5  
     1.6  lemmas [extraction_expand] =
     1.7 -  atomize_eq atomize_all atomize_imp atomize_conj
     1.8 +  meta_spec 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 eq_True eq_False
    1.11    induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq