src/HOL/Product_Type.thy
changeset 39272 0b61951d2682
parent 39198 f967a16dfcdd
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Product_Type.thy	Fri Sep 10 09:56:28 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Fri Sep 10 10:21:25 2010 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    by (simp_all add: equal)
     1.5  
     1.6  code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
     1.7 -  (Haskell infixl 4 "==")
     1.8 +  (Haskell infix 4 "==")
     1.9  
    1.10  code_instance bool :: equal
    1.11    (Haskell -)
    1.12 @@ -110,7 +110,7 @@
    1.13    (Haskell -)
    1.14  
    1.15  code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    1.16 -  (Haskell infixl 4 "==")
    1.17 +  (Haskell infix 4 "==")
    1.18  
    1.19  code_reserved SML
    1.20    unit
    1.21 @@ -281,7 +281,7 @@
    1.22    (Haskell -)
    1.23  
    1.24  code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    1.25 -  (Haskell infixl 4 "==")
    1.26 +  (Haskell infix 4 "==")
    1.27  
    1.28  types_code
    1.29    "prod"     ("(_ */ _)")