changeset 2033 | 639de962ded4 |
parent 1609 | 5324067d993f |
child 2469 | b50b8c0eec01 |
--- a/src/ZF/Cardinal_AC.ML Thu Sep 26 12:50:48 1996 +0200 +++ b/src/ZF/Cardinal_AC.ML Thu Sep 26 15:14:23 1996 +0200 @@ -34,7 +34,7 @@ "!!A. [| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] ==> \ \ |A Un C| = |B Un D|"; by (asm_full_simp_tac (ZF_ss addsimps [cardinal_eqpoll_iff, - eqpoll_disjoint_Un]) 1); + eqpoll_disjoint_Un]) 1); qed "cardinal_disjoint_Un"; goal Cardinal_AC.thy "!!A B. A lepoll B ==> |A| le |B|";