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