src/HOL/HOL.thy
changeset 7220 da6f387ca482
parent 7203 36990a7c7c72
child 7238 36e58620ffc8
     1.1 --- a/src/HOL/HOL.thy	Mon Aug 16 18:41:32 1999 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Aug 16 18:43:13 1999 +0200
     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                ("- _" [71] 70)
     1.8 +  uminus        :: ['a::minus] => 'a                ("- _" [81] 80)
     1.9    "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    1.10    (*See Nat.thy for "^"*)
    1.11