Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
new type class "zero" so that 0 can be overloaded
authorpaulson
Tue, 23 May 2000 18:22:19 +0200
changeset 8940 55bc03d9f168
parent 8939 23f85299689f
child 8941 df06883c1dcf
new type class "zero" so that 0 can be overloaded
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- 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