author | lcp |
Thu, 08 Dec 1994 16:07:12 +0100 | |
changeset 772 | 5ca7f94117bb |
parent 771 | 067767b0b35e |
child 773 | 9f8bcf1a4cff |
src/ZF/Ordinal.ML | file | annotate | diff | comparison | revisions |
--- 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";