src/ZF/Ordinal.ML

--- a/src/ZF/Ordinal.ML	Thu Dec 08 15:37:28 1994 +0100
+++ b/src/ZF/Ordinal.ML	Thu Dec 08 16:07:12 1994 +0100
@@ -238,6 +238,7 @@
 by (fast_tac (ZF_cs addSIs [Ord_succ] addSDs [Ord_succD]) 1);
 qed "le_iff";
 
+(*Equivalently, i<j ==> i < succ(j)*)
 goal Ordinal.thy "!!i j. i<j ==> i le j";
 by (asm_simp_tac (ZF_ss addsimps [le_iff]) 1);
 qed "leI";