--- a/src/HOL/Product_Type.thy Tue May 16 21:32:56 2006 +0200
+++ b/src/HOL/Product_Type.thy Tue May 16 21:33:01 2006 +0200
@@ -113,13 +113,11 @@
Times :: "['a set, 'b set] => ('a * 'b) set" (infixr "<*>" 80)
"A <*> B == Sigma A (%_. B)"
-abbreviation (xsymbols)
- Times1 (infixr "\<times>" 80)
- "Times1 == Times"
+const_syntax (xsymbols)
+ Times (infixr "\<times>" 80)
-abbreviation (HTML output)
- Times2 (infixr "\<times>" 80)
- "Times2 == Times"
+const_syntax (HTML output)
+ Times (infixr "\<times>" 80)
subsubsection {* Concrete syntax *}