--- a/src/ZF/Nat.ML Thu Jul 21 16:51:26 1994 +0200
+++ b/src/ZF/Nat.ML Tue Jul 26 13:21:20 1994 +0200
@@ -95,6 +95,15 @@
by (etac ltD 1);
val Limit_nat = result();
+goal Nat.thy "!!i. Limit(i) ==> nat le i";
+by (resolve_tac [subset_imp_le] 1);
+by (rtac subsetI 1);
+by (eresolve_tac [nat_induct] 1);
+by (fast_tac (ZF_cs addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2);
+by (REPEAT (ares_tac [Limit_has_0 RS ltD,
+ Ord_nat, Limit_is_Ord] 1));
+val nat_le_Limit = result();
+
(* succ(i): nat ==> i: nat *)
val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans;