src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Fri May 05 21:59:39 2006 +0200
+++ b/src/HOL/Nat.thy	Fri May 05 21:59:41 2006 +0200
@@ -16,17 +16,14 @@
 
 typedecl ind
 
-consts
-  Zero_Rep      :: ind
-  Suc_Rep       :: "ind => ind"
-
-axioms
+axiomatization
+  Zero_Rep :: ind and
+  Suc_Rep :: "ind => ind"
+where
   -- {* the axiom of infinity in 2 parts *}
-  inj_Suc_Rep:          "inj Suc_Rep"
+  inj_Suc_Rep:          "inj Suc_Rep" and
   Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
-finalconsts
-  Zero_Rep
-  Suc_Rep
+
 
 subsection {* Type nat *}