--- 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";
--- 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
--- 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"