src/HOL/Product_Type.thy
changeset 35427 ad039d29e01c
parent 35365 2fcd08c62495
child 35822 67e4de90d2c2
child 35828 46cfc4b8112e
     1.1 --- a/src/HOL/Product_Type.thy	Tue Mar 02 23:56:13 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Mar 02 23:59:54 2010 +0100
     1.3 @@ -142,10 +142,10 @@
     1.4      by rule+
     1.5  qed
     1.6  
     1.7 -syntax (xsymbols)
     1.8 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
     1.9 -syntax (HTML output)
    1.10 -  "*"      :: "[type, type] => type"         ("(_ \<times>/ _)" [21, 20] 20)
    1.11 +type_notation (xsymbols)
    1.12 +  "*"  ("(_ \<times>/ _)" [21, 20] 20)
    1.13 +type_notation (HTML output)
    1.14 +  "*"  ("(_ \<times>/ _)" [21, 20] 20)
    1.15  
    1.16  consts
    1.17    Pair     :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"