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