# HG changeset patch
# User wenzelm
# Date 1135359386 -3600
# Node ID beed2bc052a3a6b7eda3f02a779b3ba9fbc734af
# Parent  0a6c24f549c307c52f0d007883958b9fbf2072b7
removed obsolete induct_atomize_old;

diff -r 0a6c24f549c3 -r beed2bc052a3 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Fri Dec 23 17:37:54 2005 +0100
+++ b/src/FOL/FOL.thy	Fri Dec 23 18:36:26 2005 +0100
@@ -112,7 +112,6 @@
   shows "(A && B) == Trueprop(induct_conj(A, B))"
   by (unfold atomize_conj induct_conj_def)
 
-lemmas induct_atomize_old = induct_forall_eq induct_implies_eq induct_equal_eq atomize_conj
 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
 lemmas induct_rulify [symmetric, standard] = induct_atomize
 lemmas induct_rulify_fallback =
@@ -127,7 +126,6 @@
   structure InductMethod = InductMethodFun
   (struct
     val cases_default = thm "case_split";
-    val atomize_old = thms "induct_atomize_old";
     val atomize = thms "induct_atomize";
     val rulify = thms "induct_rulify";
     val rulify_fallback = thms "induct_rulify_fallback";
diff -r 0a6c24f549c3 -r beed2bc052a3 src/HOL/Extraction.thy
--- 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
 
diff -r 0a6c24f549c3 -r beed2bc052a3 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Dec 23 17:37:54 2005 +0100
+++ b/src/HOL/HOL.thy	Fri Dec 23 18:36:26 2005 +0100
@@ -1299,7 +1299,6 @@
   shows "(A && B) == Trueprop (induct_conj A B)"
   by (unfold atomize_conj induct_conj_def)
 
-lemmas induct_atomize_old = induct_forall_eq induct_implies_eq induct_equal_eq atomize_conj
 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
 lemmas induct_rulify [symmetric, standard] = induct_atomize
 lemmas induct_rulify_fallback =
@@ -1334,7 +1333,6 @@
   structure InductMethod = InductMethodFun
   (struct
     val cases_default = thm "case_split"
-    val atomize_old = thms "induct_atomize_old"
     val atomize = thms "induct_atomize"
     val rulify = thms "induct_rulify"
     val rulify_fallback = thms "induct_rulify_fallback"