# HG changeset patch
# User paulson
# Date 902239615 -7200
# Node ID 3087dafb70ec6ac82ae0547e0e07f7c81a1917ec
# Parent  e5129172cb2b7bf989ded5ee5364b543f7413e77
Renamed equals0D to equals0E

diff -r e5129172cb2b -r 3087dafb70ec src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Tue Aug 04 16:05:19 1998 +0200
+++ b/src/ZF/Cardinal.ML	Tue Aug 04 16:06:55 1998 +0200
@@ -635,7 +635,7 @@
                         setloop etac UnE') 1);
 by (asm_simp_tac 
     (simpset() addsimps [inj_converse_fun RS apply_funtype, right_inverse]) 1);
-by (blast_tac (claset() addEs [equals0D]) 1);
+by (blast_tac (claset() addEs [equals0E]) 1);
 qed "inj_disjoint_eqpoll";
 
 
@@ -680,6 +680,13 @@
 by (asm_full_simp_tac (simpset() addsimps [Inl_def, Inr_def]) 1);
 qed "Un_lepoll_sum";
 
+(*Krzysztof Grabczewski*)
+Goalw [eqpoll_def] "A Int B = 0 ==> A Un B eqpoll A + B";
+by (res_inst_tac [("x","lam a:A Un B. if(a:A,Inl(a),Inr(a))")] exI 1);
+by (res_inst_tac [("d","%z. case(%x. x, %x. x, z)")] lam_bijective 1);
+by (auto_tac (claset() addEs [equals0E], simpset()));
+qed "disj_Un_eqpoll_sum";
+
 
 (*** Finite and infinite sets ***)
 
diff -r e5129172cb2b -r 3087dafb70ec src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Tue Aug 04 16:05:19 1998 +0200
+++ b/src/ZF/Perm.ML	Tue Aug 04 16:06:55 1998 +0200
@@ -467,7 +467,7 @@
 by (ALLGOALS 
     (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, left_inverse] 
                          setloop (split_tac [split_if] ORELSE' etac UnE))));
-by (blast_tac (claset() addIs [inj_is_fun RS apply_type] addDs [equals0D]) 1);
+by (blast_tac (claset() addIs [inj_is_fun RS apply_type] addDs [equals0E]) 1);
 qed "inj_disjoint_Un";
 
 Goalw [surj_def]
diff -r e5129172cb2b -r 3087dafb70ec src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Tue Aug 04 16:05:19 1998 +0200
+++ b/src/ZF/ZF.ML	Tue Aug 04 16:06:55 1998 +0200
@@ -444,7 +444,7 @@
 qed_goal "equals0I" ZF.thy "[| !!y. y:A ==> False |] ==> A=0"
  (fn prems=> [ blast_tac (claset() addDs prems) 1 ]);
 
-qed_goal "equals0D" ZF.thy "!!P. [| A=0;  a:A |] ==> P"
+qed_goal "equals0E" ZF.thy "!!P. [| A=0;  a:A |] ==> P"
  (fn _=> [ Full_simp_tac 1, Blast_tac 1 ]);
 
 qed_goal "not_emptyI" ZF.thy "!!A a. a:A ==> A ~= 0"
diff -r e5129172cb2b -r 3087dafb70ec src/ZF/upair.ML
--- a/src/ZF/upair.ML	Tue Aug 04 16:05:19 1998 +0200
+++ b/src/ZF/upair.ML	Tue Aug 04 16:06:55 1998 +0200
@@ -16,7 +16,7 @@
 
 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,equals0D);       (* Pow(a)=0 ==> P *) 
+val Pow_neq_0 = Pow_top RSN (2,equals0E);       (* Pow(a)=0 ==> P *) 
 
 
 (*** Unordered pairs - Upair ***)