Default rewrite rules for quantification over Collect(A,P)

--- a/src/ZF/WF.ML	Tue Jan 07 10:19:43 1997 +0100
+++ b/src/ZF/WF.ML	Tue Jan 07 12:37:07 1997 +0100
@@ -81,9 +81,7 @@
 by (etac disjE 1);
 by (fast_tac (!claset addEs [equalityE]) 1);
 by (asm_full_simp_tac (!simpset addsimps [domainI]) 1);
-by (etac bexE 1);
-by (dtac minor 1);
-by (Fast_tac 1);
+by (fast_tac (!claset addSDs [minor]) 1);
 qed "wf_induct";
 
 (*Perform induction on i, then prove the wf(r) subgoal using prems. *)

--- a/src/ZF/simpdata.ML	Tue Jan 07 10:19:43 1997 +0100
+++ b/src/ZF/simpdata.ML	Tue Jan 07 12:37:07 1997 +0100
@@ -15,15 +15,23 @@
                       (fast_tac (!claset addSIs [equalityI]) 1) ]));
 
 (*Are all these really suitable?*)
-Addsimps (map prove_fun
-	  ["(ALL x:0.P(x)) <-> True",
-	   "(EX  x:0.P(x)) <-> False",
-	   "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
-	   "(EX  x:succ(i).P(x)) <-> P(i) | (EX  x:i.P(x))",
-	   "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))",
-	   "(EX  x:cons(a,B).P(x)) <-> P(a) | (EX  x:B.P(x))",
-	   "(ALL x: RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
-	   "(EX  x: RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))"]);
+val ball_simps = map prove_fun
+    ["(ALL x:0.P(x)) <-> True",
+     "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
+     "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))",
+     "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
+     "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
+     "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"];
+
+val bex_simps = map prove_fun
+    ["(EX x:0.P(x)) <-> False",
+     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))",
+     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B.P(x))",
+     "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
+     "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
+     "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"];
+
+Addsimps (ball_simps @ bex_simps);
 
 Addsimps (map prove_fun
 	  ["{x:0. P(x)} = 0",