src/ZF/Cardinal_AC.ML

--- a/src/ZF/Cardinal_AC.ML	Tue Nov 29 00:31:31 1994 +0100
+++ b/src/ZF/Cardinal_AC.ML	Tue Nov 29 11:51:07 1994 +0100
@@ -144,6 +144,8 @@
 by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
 val lt_subset_trans = result();
 
+(*The same yet again, but the index set need not be a cardinal.  
+  Surprisingly complicated proof!*)
 goal Cardinal_AC.thy
     "!!K. [| InfCard(K);  |W| le K;  ALL w:W. j(w) < csucc(K) |] ==> \
 \         (UN w:W. j(w)) < csucc(K)";