src/HOL/Extraction.thy
changeset 18511 beed2bc052a3
parent 18456 8cc35e95450a
child 18708 4b3dadb4fe33
     1.1 --- a/src/HOL/Extraction.thy	Fri Dec 23 17:37:54 2005 +0100
     1.2 +++ b/src/HOL/Extraction.thy	Fri Dec 23 18:36:26 2005 +0100
     1.3 @@ -54,7 +54,7 @@
     1.4    notE' impE' impE iffE imp_cong simp_thms
     1.5    induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
     1.6    induct_forall_def induct_implies_def induct_equal_def induct_conj_def
     1.7 -  induct_atomize induct_atomize_old induct_rulify induct_rulify_fallback
     1.8 +  induct_atomize induct_rulify induct_rulify_fallback
     1.9  
    1.10  datatype sumbool = Left | Right
    1.11