--- a/src/CCL/Set.ML Thu Dec 15 18:13:40 2005 +0100
+++ b/src/CCL/Set.ML Thu Dec 15 19:42:00 2005 +0100
@@ -143,15 +143,6 @@
by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
qed "equalityCE";
-(*Lemma for creating induction formulae -- for "pattern matching" on p
- To make the induction hypotheses usable, apply "spec" or "bspec" to
- put universal quantifiers over the free variables in p. *)
-val prems = goal (the_context ())
- "[| p:A; !!z. z:A ==> p=z --> R |] ==> R";
-by (rtac mp 1);
-by (REPEAT (resolve_tac (refl::prems) 1));
-qed "setup_induction";
-
Goal "{x. x:A} = A";
by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1 ORELSE etac CollectD 1));
qed "trivial_set";
--- a/src/HOL/Induct/SList.thy Thu Dec 15 18:13:40 2005 +0100
+++ b/src/HOL/Induct/SList.thy Thu Dec 15 19:42:00 2005 +0100
@@ -295,9 +295,7 @@
lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard]
lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
-apply (erule setup_induction)
-apply (erule list.induct, blast+)
-done
+ by (induct L == "CONS M N" set: list) auto
lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
apply (simp add: CONS_def In1_def)
--- a/src/HOL/Induct/Sexp.thy Thu Dec 15 18:13:40 2005 +0100
+++ b/src/HOL/Induct/Sexp.thy Thu Dec 15 19:42:00 2005 +0100
@@ -65,9 +65,7 @@
by blast
lemma Scons_D: "Scons M N \<in> sexp ==> M \<in> sexp & N \<in> sexp"
-apply (erule setup_induction)
-apply (erule sexp.induct, blast+)
-done
+ by (induct S == "Scons M N" set: sexp) auto
(** Introduction rules for 'pred_sexp' **)
--- a/src/HOL/Set.ML Thu Dec 15 18:13:40 2005 +0100
+++ b/src/HOL/Set.ML Thu Dec 15 19:42:00 2005 +0100
@@ -351,7 +351,6 @@
val set_diff_def = thm "set_diff_def";
val set_eq_subset = thm "set_eq_subset";
val set_ext = thm "set_ext";
-val setup_induction = thm "setup_induction";
val singletonD = thm "singletonD";
val singletonE = thm "singletonE";
val singletonI = thm "singletonI";
--- a/src/HOL/Set.thy Thu Dec 15 18:13:40 2005 +0100
+++ b/src/HOL/Set.thy Thu Dec 15 19:42:00 2005 +0100
@@ -566,16 +566,6 @@
"A = B ==> (c \<in> A ==> c \<in> B ==> P) ==> (c \<notin> A ==> c \<notin> B ==> P) ==> P"
by blast
-text {*
- \medskip Lemma for creating induction formulae -- for "pattern
- matching" on @{text p}. To make the induction hypotheses usable,
- apply @{text spec} or @{text bspec} to put universal quantifiers over the free
- variables in @{text p}.
-*}
-
-lemma setup_induction: "p:A ==> (!!z. z:A ==> p = z --> R) ==> R"
- by simp
-
lemma eqset_imp_iff: "A = B ==> (x : A) = (x : B)"
by simp
--- a/src/ZF/ZF.thy Thu Dec 15 18:13:40 2005 +0100
+++ b/src/ZF/ZF.thy Thu Dec 15 19:42:00 2005 +0100
@@ -425,14 +425,6 @@
"[| A = B; [| c\<in>A; c\<in>B |] ==> P; [| c~:A; c~:B |] ==> P |] ==> P"
by (erule equalityE, blast)
-(*Lemma for creating induction formulae -- for "pattern matching" on p
- To make the induction hypotheses usable, apply "spec" or "bspec" to
- put universal quantifiers over the free variables in p.
- Would it be better to do subgoal_tac "\<forall>z. p = f(z) --> R(z)" ??*)
-lemma setup_induction: "[| p: A; !!z. z: A ==> p=z --> R |] ==> R"
-by auto
-
-
subsection{*Rules for Replace -- the derived form of replacement*}
@@ -696,7 +688,6 @@
val equalityD2 = thm "equalityD2";
val equalityE = thm "equalityE";
val equalityCE = thm "equalityCE";
-val setup_induction = thm "setup_induction";
val Replace_iff = thm "Replace_iff";
val ReplaceI = thm "ReplaceI";
val ReplaceE = thm "ReplaceE";