author | wenzelm |
Wed, 01 Sep 1999 21:24:50 +0200 | |
changeset 7426 | e0be36ee7ab9 |
parent 7425 | 2089c70f2c6d |
child 7427 | e5a5d59dd513 |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- 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 "^"*)