src/HOL/HOL.thy
changeset 5786 9a2c90bdadfe
parent 5492 d9fc3457554e
child 6027 9dd06eeda95c
     1.1 --- a/src/HOL/HOL.thy	Sat Oct 31 12:46:21 1998 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Nov 02 12:35:14 1998 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4  consts
     1.5    "+"           :: ['a::plus, 'a]  => 'a            (infixl 65)
     1.6    "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
     1.7 -  uminus        :: ['a::minus] => 'a                ("- _" [80] 80)
     1.8 +  uminus        :: ['a::minus] => 'a                ("- _" [100] 100)
     1.9    "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    1.10    (*See Nat.thy for "^"*)
    1.11