changeset 7426 | e0be36ee7ab9 |
parent 7369 | 2d2110cda81e |
child 8473 | 2798d2f71ec2 |
--- a/src/HOL/HOL.thy Wed Sep 01 21:24:23 1999 +0200 +++ b/src/HOL/HOL.thy Wed Sep 01 21:24:50 1999 +0200 @@ -62,7 +62,7 @@ "+" :: "['a::plus, 'a] => 'a" (infixl 65) - :: "['a::minus, 'a] => 'a" (infixl 65) uminus :: "['a::minus] => 'a" ("- _" [81] 80) - "*" :: "['a::times, 'a] => 'a" (infixl 70) + * :: "['a::times, 'a] => 'a" (infixl 70) (*See Nat.thy for "^"*)