# HG changeset patch
# User paulson
# Date 959098939 -7200
# Node ID 55bc03d9f168cba5db827a2e729c5a4e023a431e
# Parent  23f85299689fda5a3a2ae8628e8ffe028c71f85e
new type class "zero" so that 0 can be overloaded

diff -r 23f85299689f -r 55bc03d9f168 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue May 23 18:21:51 2000 +0200
+++ b/src/HOL/HOL.thy	Tue May 23 18:22:19 2000 +0200
@@ -53,12 +53,14 @@
 
 (* Overloaded Constants *)
 
-axclass plus < "term"
+axclass zero  < "term" 
+axclass plus  < "term"
 axclass minus < "term"
 axclass times < "term"
 axclass power < "term"
 
 consts
+  "0"           :: "('a::zero)"                     ("0")
   "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
   -             :: "['a::minus, 'a] => 'a"          (infixl 65)
   uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)