# HG changeset patch
# User paulson
# Date 1025256261 -7200
# Node ID 8c79a0dce4c0f32e555e1bca768f3b9d5fde5116
# Parent  74cb2af8811eef63b1d895630137aef58e66d69a
tweaked

diff -r 74cb2af8811e -r 8c79a0dce4c0 src/ZF/WF.thy
--- a/src/ZF/WF.thy	Wed Jun 26 18:31:20 2002 +0200
+++ b/src/ZF/WF.thy	Fri Jun 28 11:24:21 2002 +0200
@@ -99,13 +99,13 @@
 
 (** Well-founded Induction **)
 
-(*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)
+(*Consider the least z in domain(r) such that P(z) does not hold...*)
 lemma wf_induct:
     "[| wf(r);
         !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x)
      |]  ==>  P(a)"
 apply (unfold wf_def) 
-apply (erule_tac x = "{z:domain (r) Un {a}. ~P (z) }" in allE)
+apply (erule_tac x = "{z : domain(r). ~ P(z)}" in allE)
 apply blast 
 done
 
@@ -134,14 +134,6 @@
 apply (rule field_Int_square, blast)
 done
 
-text{*The assumption @{term "r \<subseteq> A*A"} justifies strengthening the induction
-      hypothesis by removing the restriction to @{term A}.*}
-lemma wf_on_induct2:
-    "[| wf[A](r);  a:A;  r \<subseteq> A*A; 
-        !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x)
-     |]  ==>  P(a)"
-by (rule wf_on_induct, assumption+, blast)
-
 (*fixed up for induct method*)
 lemmas wf_on_induct = wf_on_induct [consumes 2, induct set: wf_on]
    and wf_on_induct_rule =