| changeset 37 | cebe01deba80 |
| parent 27 | 0e152fe9571e |
| child 187 | 8729bfdcb638 |
--- a/src/ZF/Univ.ML Thu Oct 07 09:49:46 1993 +0100 +++ b/src/ZF/Univ.ML Thu Oct 07 10:48:16 1993 +0100 @@ -185,7 +185,7 @@ val Limit_nat = result(); goalw Univ.thy [Limit_def] - "!!i. [| 0<i; ALL y. ~ succ(y)=i |] ==> Limit(i)"; + "!!i. [| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)"; by (safe_tac subset_cs); by (rtac (not_le_iff_lt RS iffD1) 2); by (fast_tac (lt_cs addEs [lt_anti_sym]) 4);