src/ZF/Cardinal_AC.ML
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|";