# HG changeset patch
# User wenzelm
# Date 1134672120 -3600
# Node ID 50c0c118e96db6e0ff7e4a3e41a8ed00e40847fc
# Parent  9f6b3e1da3520b9835749674ed82adfe4d6f0428
removed obsolete/unused setup_induction;

diff -r 9f6b3e1da352 -r 50c0c118e96d src/CCL/Set.ML
--- 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";
diff -r 9f6b3e1da352 -r 50c0c118e96d src/HOL/Induct/SList.thy
--- 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)
diff -r 9f6b3e1da352 -r 50c0c118e96d src/HOL/Induct/Sexp.thy
--- 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' **)
 
diff -r 9f6b3e1da352 -r 50c0c118e96d src/HOL/Set.ML
--- 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";
diff -r 9f6b3e1da352 -r 50c0c118e96d src/HOL/Set.thy
--- 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
 
diff -r 9f6b3e1da352 -r 50c0c118e96d src/ZF/ZF.thy
--- 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";