# HG changeset patch
# User paulson
# Date 959099357 -7200
# Node ID a4f8be72f585e6eea7d17257c4d66ce50177b35b
# Parent  6aad5381ba83a4681d9ce2c535e41ab363a2f303
now 0 is overloaded

diff -r 6aad5381ba83 -r a4f8be72f585 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"