| changeset 37 | cebe01deba80 |
| parent 30 | d49df4181f0d |
| child 186 | 320f6bdb593a |
--- a/src/ZF/ord.ML Thu Oct 07 09:49:46 1993 +0100 +++ b/src/ZF/ord.ML Thu Oct 07 10:48:16 1993 +0100 @@ -380,7 +380,7 @@ by (REPEAT (resolve_tac [Ord_0, not_lt0] 1)); val Ord_0_le = result(); -goal Ord.thy "!!i. [| Ord(i); ~ i=0 |] ==> 0<i"; +goal Ord.thy "!!i. [| Ord(i); i~=0 |] ==> 0<i"; by (etac (not_le_iff_lt RS iffD1) 1); by (rtac Ord_0 1); by (fast_tac lt_cs 1);