# HG changeset patch
# User paulson
# Date 857468493 -3600
# Node ID 9e11a914156af260fd6c864162f9add74331f95e
# Parent  79c35a0511963bea1150537d0bd49462e2120854
Now uses RepFun_eqI instead of RepFunI;
improved version of InterE to replace "make_elim InterD" in claset

diff -r 79c35a051196 -r 9e11a914156a src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Tue Mar 04 10:21:16 1997 +0100
+++ b/src/ZF/ZF.ML	Tue Mar 04 10:41:33 1997 +0100
@@ -256,7 +256,7 @@
   [ (rtac (major RS ReplaceE) 1),
     (REPEAT (ares_tac prems 1)) ]);
 
-AddIs  [RepFunI];  
+AddIs  [RepFun_eqI];  
 AddSEs [RepFunE];
 
 qed_goalw "RepFun_cong" ZF.thy [RepFun_def]
@@ -375,13 +375,13 @@
 
 (*"Classical" elimination rule -- does not require exhibiting B:C *)
 qed_goalw "InterE" ZF.thy [Inter_def]
-    "[| A : Inter(C);  A:B ==> R;  B~:C ==> R |] ==> R"
+    "[| A : Inter(C);  B~:C ==> R;  A:B ==> R |] ==> R"
  (fn major::prems=>
   [ (rtac (major RS CollectD2 RS ballE) 1),
     (REPEAT (eresolve_tac prems 1)) ]);
 
 AddSIs [InterI];
-AddEs  [InterD, make_elim InterD];
+AddEs  [InterD, InterE];
 
 (*** Rules for Intersections of families ***)
 (* INT x:A. B(x) abbreviates Inter({B(x). x:A}) *)