| changeset 21210 | c17fd2df4e9e |
| parent 21195 | 0cca8d19557d |
| child 21331 | 1fd8ba48ae97 |
--- a/src/HOL/Product_Type.thy Tue Nov 07 11:47:56 2006 +0100 +++ b/src/HOL/Product_Type.thy Tue Nov 07 11:47:57 2006 +0100 @@ -113,10 +113,10 @@ Times :: "['a set, 'b set] => ('a * 'b) set" (infixr "<*>" 80) "A <*> B == Sigma A (%_. B)" -const_syntax (xsymbols) +notation (xsymbols) Times (infixr "\<times>" 80) -const_syntax (HTML output) +notation (HTML output) Times (infixr "\<times>" 80)