leI: added comment
authorlcp
Thu, 08 Dec 1994 16:07:12 +0100
changeset 772 5ca7f94117bb
parent 771 067767b0b35e
child 773 9f8bcf1a4cff
leI: added comment
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";