# HG changeset patch
# User paulson
# Date 858764966 -3600
# Node ID c05fa3ce5439d12b3e0f2864abc6af36997780c0
# Parent  a318f7f3a65cc6a9e4793abe9d658d3b6437ec5b
Improved intersection rule InterI: now truly safe, since the unsafeness is
delegated to exI.

diff -r a318f7f3a65c -r c05fa3ce5439 src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Wed Mar 19 10:24:39 1997 +0100
+++ b/src/ZF/ZF.ML	Wed Mar 19 10:49:26 1997 +0100
@@ -363,9 +363,10 @@
  (fn _=> [ Simp_tac 1, Fast_tac 1 ]);
 
 (* Intersection is well-behaved only if the family is non-empty! *)
-qed_goalw "InterI" ZF.thy [Inter_def]
-    "[| !!x. x: C ==> A: x;  c:C |] ==> A : Inter(C)"
- (fn prems=> [ fast_tac (!claset addIs prems) 1 ]);
+qed_goal "InterI" ZF.thy
+    "[| !!x. x: C ==> A: x;  EX c. c:C |] ==> A : Inter(C)"
+ (fn prems=> [ (simp_tac (!simpset addsimps [Inter_iff]) 1), 
+	       Cla.fast_tac (!claset addIs prems) 1 ]);
 
 (*A "destruct" rule -- every B in C contains A as an element, but
   A:B can hold when B:C does not!  This rule is analogous to "spec". *)
@@ -464,7 +465,7 @@
 (*The search is undirected; similar proof attempts may fail.
   b represents ANY map, such as (lam x:A.b(x)): A->Pow(A). *)
 qed_goal "cantor" ZF.thy "EX S: Pow(A). ALL x:A. b(x) ~= S"
- (fn _ => [best_tac cantor_cs 1]);
+ (fn _ => [Cla.best_tac cantor_cs 1]);
 
 (*Lemma for the inductive definition in Zorn.thy*)
 qed_goal "Union_in_Pow" ZF.thy