src/ZF/Cardinal.ML

--- a/src/ZF/Cardinal.ML	Wed May 01 10:35:06 1996 +0200
+++ b/src/ZF/Cardinal.ML	Wed May 01 10:37:07 1996 +0200
@@ -120,6 +120,11 @@
 by (fast_tac (ZF_cs addIs [lepoll_0_is_0, lepoll_refl]) 1);
 qed "lepoll_0_iff";
 
+goalw Cardinal.thy [lepoll_def] 
+    "!!A. [| A lepoll B; C lepoll D; B Int D = 0 |] ==> A Un C lepoll B Un D";
+by (fast_tac (ZF_cs addIs [inj_disjoint_Un]) 1);
+qed "Un_lepoll_Un";
+
 (*A eqpoll 0 ==> A=0*)
 bind_thm ("eqpoll_0_is_0",  eqpoll_imp_lepoll RS lepoll_0_is_0);