Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOL.thy
changeset 8940 55bc03d9f168
parent 8800 e3688ef49f12
child 8959 9d793220a46a 
--- 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)
isabelle