src/HOL/Product_Type.thy
changeset 61955 e96292f32c3c
parent 61943 7fba644ed827
child 62101 26c0a70f78a3
     1.1 --- a/src/HOL/Product_Type.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -226,11 +226,11 @@
     1.4  
     1.5  definition "prod = {f. \<exists>a b. f = Pair_Rep (a::'a) (b::'b)}"
     1.6  
     1.7 -typedef ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
     1.8 +typedef ('a, 'b) prod ("(_ \<times>/ _)" [21, 20] 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
     1.9    unfolding prod_def by auto
    1.10  
    1.11 -type_notation (xsymbols)
    1.12 -  "prod"  ("(_ \<times>/ _)" [21, 20] 20)
    1.13 +type_notation (ASCII)
    1.14 +  prod  (infixr "*" 20)
    1.15  
    1.16  definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
    1.17    "Pair a b = Abs_prod (Pair_Rep a b)"