equal
deleted
inserted
replaced
183 by (safe_tac (ZF_cs addSIs (ltI::nat_typechecks))); |
183 by (safe_tac (ZF_cs addSIs (ltI::nat_typechecks))); |
184 by (etac ltD 1); |
184 by (etac ltD 1); |
185 val Limit_nat = result(); |
185 val Limit_nat = result(); |
186 |
186 |
187 goalw Univ.thy [Limit_def] |
187 goalw Univ.thy [Limit_def] |
188 "!!i. [| 0<i; ALL y. ~ succ(y)=i |] ==> Limit(i)"; |
188 "!!i. [| 0<i; ALL y. succ(y) ~= i |] ==> Limit(i)"; |
189 by (safe_tac subset_cs); |
189 by (safe_tac subset_cs); |
190 by (rtac (not_le_iff_lt RS iffD1) 2); |
190 by (rtac (not_le_iff_lt RS iffD1) 2); |
191 by (fast_tac (lt_cs addEs [lt_anti_sym]) 4); |
191 by (fast_tac (lt_cs addEs [lt_anti_sym]) 4); |
192 by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1)); |
192 by (REPEAT (eresolve_tac [asm_rl, ltE, Ord_succ] 1)); |
193 val non_succ_LimitI = result(); |
193 val non_succ_LimitI = result(); |