src/HOL/HOL.thy
changeset 8940 55bc03d9f168
parent 8800 e3688ef49f12
child 8959 9d793220a46a
     1.1 --- a/src/HOL/HOL.thy	Tue May 23 18:21:51 2000 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue May 23 18:22:19 2000 +0200
     1.3 @@ -53,12 +53,14 @@
     1.4  
     1.5  (* Overloaded Constants *)
     1.6  
     1.7 -axclass plus < "term"
     1.8 +axclass zero  < "term" 
     1.9 +axclass plus  < "term"
    1.10  axclass minus < "term"
    1.11  axclass times < "term"
    1.12  axclass power < "term"
    1.13  
    1.14  consts
    1.15 +  "0"           :: "('a::zero)"                     ("0")
    1.16    "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
    1.17    -             :: "['a::minus, 'a] => 'a"          (infixl 65)
    1.18    uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)