src/HOL/NatDef.thy

--- a/src/HOL/NatDef.thy	Tue May 23 18:28:11 2000 +0200
+++ b/src/HOL/NatDef.thy	Tue May 23 18:29:17 2000 +0200
@@ -39,13 +39,12 @@
   nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))"   (lfp_def)
 
 instance
-  nat :: ord
+  nat :: {ord, zero}
 
 
 (* abstract constants and syntax *)
 
 consts
-  "0"       :: nat                ("0")
   Suc       :: nat => nat
   pred_nat  :: "(nat * nat) set"