src/ZF/Finite.thy

--- a/src/ZF/Finite.thy	Tue Aug 01 13:43:22 2000 +0200
+++ b/src/ZF/Finite.thy	Tue Aug 01 15:28:21 2000 +0200
@@ -6,7 +6,18 @@
 Finite powerset operator
 *)
 
-Finite = Arith + Inductive +
+Finite = Inductive + Nat +
+
+setup setup_datatypes
+
+(*The natural numbers as a datatype*)
+rep_datatype 
+  elim		natE
+  induct	nat_induct
+  case_eqns	nat_case_0, nat_case_succ
+  recursor_eqns recursor_0, recursor_succ
+
+
 consts
   Fin       :: i=>i
   FiniteFun :: [i,i]=>i         ("(_ -||>/ _)" [61, 60] 60)