src/ZF/ZF.ML

--- a/src/ZF/ZF.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ZF.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -152,6 +152,8 @@
 qed_goal "equalityI" ZF.thy "[| A <= B;  B <= A |] ==> A = B"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[conjI, extension RS iffD2]) 1)) ]);
 
+AddIs [equalityI];
+
 qed_goal "equality_iffI" ZF.thy "(!!x. x:A <-> x:B) ==> A = B"
  (fn [prem] =>
   [ (rtac equalityI 1),
@@ -268,7 +270,7 @@
  (fn _ => [Fast_tac 1]);
 
 goal ZF.thy "{x.x:A} = A";
-by (fast_tac (!claset addSIs [equalityI]) 1);
+by (fast_tac (!claset) 1);
 qed "triv_RepFun";
 
 Addsimps [RepFun_iff, triv_RepFun];
@@ -438,7 +440,7 @@
 AddSIs [empty_subsetI];
 
 qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
- (fn prems=> [ fast_tac (!claset addIs [equalityI] addDs prems) 1 ]);
+ (fn prems=> [ fast_tac (!claset addDs prems) 1 ]);
 
 qed_goal "equals0D" ZF.thy "!!P. [| A=0;  a:A |] ==> P"
  (fn _=> [ Full_simp_tac 1, Fast_tac 1 ]);