src/HOL/HOL.thy
changeset 8800 e3688ef49f12
parent 8640 2f9b008a27a1
child 8940 55bc03d9f168
     1.1 --- a/src/HOL/HOL.thy	Fri May 05 17:49:54 2000 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri May 05 18:24:06 2000 +0200
     1.3 @@ -62,6 +62,7 @@
     1.4    "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
     1.5    -             :: "['a::minus, 'a] => 'a"          (infixl 65)
     1.6    uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
     1.7 +  abs		:: "('a::minus) => 'a"
     1.8    *             :: "['a::times, 'a] => 'a"          (infixl 70)
     1.9    (*See Nat.thy for "^"*)
    1.10