src/ZF/Ordinal.ML

--- a/src/ZF/Ordinal.ML	Tue Mar 26 11:42:36 1996 +0100
+++ b/src/ZF/Ordinal.ML	Tue Mar 26 11:45:54 1996 +0100
@@ -436,6 +436,7 @@
 by (asm_simp_tac (ZF_ss addsimps [not_lt_iff_le RS iff_sym]) 1);
 qed "not_le_iff_lt";
 
+(*This is identical to 0<succ(i) *)
 goal Ordinal.thy "!!i. Ord(i) ==> 0 le i";
 by (etac (not_lt_iff_le RS iffD1) 1);
 by (REPEAT (resolve_tac [Ord_0, not_lt0] 1));