src/HOL/Product_Type.thy
changeset 19656 09be06943252
parent 19535 e4fdeb32eadf
child 20044 92cc2f4c7335
     1.1 --- a/src/HOL/Product_Type.thy	Tue May 16 21:32:56 2006 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Tue May 16 21:33:01 2006 +0200
     1.3 @@ -113,13 +113,11 @@
     1.4    Times :: "['a set, 'b set] => ('a * 'b) set"  (infixr "<*>" 80)
     1.5    "A <*> B == Sigma A (%_. B)"
     1.6  
     1.7 -abbreviation (xsymbols)
     1.8 -  Times1  (infixr "\<times>" 80)
     1.9 -  "Times1 == Times"
    1.10 +const_syntax (xsymbols)
    1.11 +  Times  (infixr "\<times>" 80)
    1.12  
    1.13 -abbreviation (HTML output)
    1.14 -  Times2  (infixr "\<times>" 80)
    1.15 -  "Times2 == Times"
    1.16 +const_syntax (HTML output)
    1.17 +  Times  (infixr "\<times>" 80)
    1.18  
    1.19  
    1.20  subsubsection {* Concrete syntax *}