# HG changeset patch
# User wenzelm
# Date 1146859181 -7200
# Node ID 340c466c96051a9927c2967b28bbb52f5ac4eea5
# Parent  a4b3176f19dd1cda64fd0fe26e3509ca8d511bb4
axiomatization;

diff -r a4b3176f19dd -r 340c466c9605 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 *}