# HG changeset patch
# User lcp
# Date 788196635 -3600
# Node ID ba28811c34967299ea5a301503250486409c983a
# Parent  03d7bfa70289ddf5393bccbf2de2156b4b2e3340
natE0: deleted, since unused

diff -r 03d7bfa70289 -r ba28811c3496 src/ZF/Nat.ML
--- a/src/ZF/Nat.ML	Fri Dec 23 16:29:53 1994 +0100
+++ b/src/ZF/Nat.ML	Fri Dec 23 16:30:35 1994 +0100
@@ -35,6 +35,10 @@
 by (rtac (nat_0I RS nat_succI) 1);
 qed "nat_1I";
 
+goal Nat.thy "2 : nat";
+by (rtac (nat_1I RS nat_succI) 1);
+qed "nat_2I";
+
 goal Nat.thy "bool <= nat";
 by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1
 	    ORELSE eresolve_tac [boolE,ssubst] 1));
@@ -75,12 +79,6 @@
 
 val nat_le_refl = nat_into_Ord RS le_refl;
 
-goal Nat.thy "!!n. n: nat ==> n=0 | 0:n";
-by (etac nat_induct 1);
-by (fast_tac ZF_cs 1);
-by (fast_tac (ZF_cs addIs [nat_0_le]) 1);
-qed "natE0";
-
 goal Nat.thy "Ord(nat)";
 by (rtac OrdI 1);
 by (etac (nat_into_Ord RS Ord_is_Transset) 2);