# HG changeset patch
# User nipkow
# Date 907063272 -7200
# Node ID 354f4914811f262bee9a30ec0d2551d706b72358
# Parent  32f99ca617b7c827a1dc23ee1d3ec1c857fa2bf6
Revised wf_acc_iff and Co.

diff -r 32f99ca617b7 -r 354f4914811f src/HOL/Induct/Acc.ML
--- a/src/HOL/Induct/Acc.ML	Tue Sep 29 12:00:52 1998 +0200
+++ b/src/HOL/Induct/Acc.ML	Tue Sep 29 12:01:12 1998 +0200
@@ -43,28 +43,17 @@
 by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
 qed "acc_induct";
 
-
-Goal "r <= (acc r) Times (acc r) ==> wf(r)";
-by (etac wfI 1);
-by (etac acc.induct 1);
-by (rewtac pred_def);
-by (Fast_tac 1);
+Goal "!x. x : acc(r) ==> wf(r)";
+by (rtac wfUNIVI 1);
+by(deepen_tac (claset() addEs [acc_induct]) 1 1);
 qed "acc_wfI";
 
-Goal "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
+Goal "wf(r) ==> x : acc(r)";
 by (etac wf_induct 1);
-by (rtac (impI RS allI) 1);
 by (rtac accI 1);
-by (Fast_tac 1);
-qed "acc_wfD_lemma";
-
-Goal "wf(r) ==> r <= (acc r) Times (acc r)";
-by (rtac subsetI 1);
-by (res_inst_tac [("p", "x")] PairE 1);
-by (fast_tac (claset() addSIs [SigmaI,
-			       acc_wfD_lemma RS spec RS mp]) 1);
+by (Blast_tac 1);
 qed "acc_wfD";
 
-Goal "wf(r)  =  (r <= (acc r) Times (acc r))";
-by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
+Goal "wf(r)  =  (!x. x : acc(r))";
+by (blast_tac (claset() addIs [acc_wfI] addDs [acc_wfD]) 1);
 qed "wf_acc_iff";