# HG changeset patch
# User lcp
# Date 786899232 -3600
# Node ID 5ca7f94117bbf3eaca601253d67f186af8578c57
# Parent  067767b0b35e53ba759323e7fe170aba5c327fb8
leI: added comment

diff -r 067767b0b35e -r 5ca7f94117bb 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";