# HG changeset patch
# User paulson
# Date 905442003 -7200
# Node ID 079d8eb6db1989200b289d5d41d0d9b1fd395c02
# Parent  f864dbcda5f1c53e64f44b8db2aeef3a7e6cfb9e
tidied

diff -r f864dbcda5f1 -r 079d8eb6db19 src/ZF/upair.ML
--- a/src/ZF/upair.ML	Thu Sep 10 17:38:36 1998 +0200
+++ b/src/ZF/upair.ML	Thu Sep 10 17:40:03 1998 +0200
@@ -16,14 +16,13 @@
 
 val Pow_bottom = empty_subsetI RS PowI;         (* 0 : Pow(B) *)
 val Pow_top = subset_refl RS PowI;              (* A : Pow(A) *)
-val Pow_neq_0 = Pow_top RSN (2,equals0E);       (* Pow(a)=0 ==> P *) 
 
 
 (*** Unordered pairs - Upair ***)
 
 qed_goalw "Upair_iff" thy [Upair_def]
     "c : Upair(a,b) <-> (c=a | c=b)"
- (fn _ => [ (blast_tac (claset() addEs [Pow_neq_0, sym RS Pow_neq_0]) 1) ]);
+ (fn _ => [ (Blast_tac 1) ]);
 
 Addsimps [Upair_iff];