# HG changeset patch
# User lcp
# Date 775392280 -7200
# Node ID 3686157a5a514838cf0c5f79f086d7ca36a6abe0
# Parent  e2f00c943fa522be4010b7ac15af3c8395c4e6a2
ZF/WF/wf_induct: streamlined proof

diff -r e2f00c943fa5 -r 3686157a5a51 src/ZF/WF.ML
--- a/src/ZF/WF.ML	Thu Jul 28 11:25:37 1994 +0200
+++ b/src/ZF/WF.ML	Thu Jul 28 12:44:40 1994 +0200
@@ -73,19 +73,16 @@
 (** Well-founded Induction **)
 
 (*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*)
-val major::prems = goalw WF.thy [wf_def]
+val [major,minor] = goalw WF.thy [wf_def]
     "[| wf(r);          \
 \       !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \
 \    |]  ==>  P(a)";
 by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ]  (major RS allE) 1);
 by (etac disjE 1);
-by (rtac classical 1);
-by (etac equals0D 1);
-by (etac (singletonI RS UnI2 RS CollectI) 1);
+by (fast_tac (ZF_cs addEs [equalityE]) 1);
+by (asm_full_simp_tac (ZF_ss addsimps [domainI]) 1);
 by (etac bexE 1);
-by (etac CollectE 1);
-by (etac swap 1);
-by (resolve_tac prems 1);
+by (dtac minor 1);
 by (fast_tac ZF_cs 1);
 val wf_induct = result();