src/HOL/HOL.thy
changeset 8940 55bc03d9f168
parent 8800 e3688ef49f12
child 8959 9d793220a46a
equal deleted inserted replaced
8939:23f85299689f 8940:55bc03d9f168
    51   -->           :: "[bool, bool] => bool"           (infixr 25)
    51   -->           :: "[bool, bool] => bool"           (infixr 25)
    52 
    52 
    53 
    53 
    54 (* Overloaded Constants *)
    54 (* Overloaded Constants *)
    55 
    55 
    56 axclass plus < "term"
    56 axclass zero  < "term" 
       
    57 axclass plus  < "term"
    57 axclass minus < "term"
    58 axclass minus < "term"
    58 axclass times < "term"
    59 axclass times < "term"
    59 axclass power < "term"
    60 axclass power < "term"
    60 
    61 
    61 consts
    62 consts
       
    63   "0"           :: "('a::zero)"                     ("0")
    62   "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
    64   "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
    63   -             :: "['a::minus, 'a] => 'a"          (infixl 65)
    65   -             :: "['a::minus, 'a] => 'a"          (infixl 65)
    64   uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
    66   uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
    65   abs		:: "('a::minus) => 'a"
    67   abs		:: "('a::minus) => 'a"
    66   *             :: "['a::times, 'a] => 'a"          (infixl 70)
    68   *             :: "['a::times, 'a] => 'a"          (infixl 70)