# HG changeset patch
# User haftmann
# Date 1284106885 -7200
# Node ID 0b61951d26828a082340dbfb110ed29b21595ccf
# Parent  436554f1beaaf0e243e812421bec5ca9743392da
Haskell == is infix, not infixl

diff -r 436554f1beaa -r 0b61951d2682 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Sep 10 10:21:25 2010 +0200
@@ -345,7 +345,7 @@
 code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
   (SML "!((_ : Int.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
   (Scala infixl 5 "==")
   (Eval "!((_ : int) = _)")
 
diff -r 436554f1beaa -r 0b61951d2682 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/HOL.thy	Fri Sep 10 10:21:25 2010 +0200
@@ -1942,10 +1942,10 @@
   (Haskell "Eq")
 
 code_const "HOL.equal"
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
 
 code_const HOL.eq
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
 
 text {* undefined *}
 
diff -r 436554f1beaa -r 0b61951d2682 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy	Fri Sep 10 10:21:25 2010 +0200
@@ -34,7 +34,7 @@
 code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (SML "!((_ : char) = _)")
   (OCaml "!((_ : char) = _)")
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
   (Scala infixl 5 "==")
 
 code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
diff -r 436554f1beaa -r 0b61951d2682 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Fri Sep 10 10:21:25 2010 +0200
@@ -99,7 +99,7 @@
 code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
   (Scala infixl 5 "==")
   (Eval infixl 6 "=")
 
diff -r 436554f1beaa -r 0b61951d2682 src/HOL/Library/Code_Natural.thy
--- a/src/HOL/Library/Code_Natural.thy	Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy	Fri Sep 10 10:21:25 2010 +0200
@@ -130,7 +130,7 @@
   (Scala infixl 8 "/%")
 
 code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
   (Scala infixl 5 "==")
 
 code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
diff -r 436554f1beaa -r 0b61951d2682 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Sep 10 10:21:25 2010 +0200
@@ -443,7 +443,7 @@
 code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
   (Scala infixl 5 "==")
   (Eval infixl 6 "=")
 
diff -r 436554f1beaa -r 0b61951d2682 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/List.thy	Fri Sep 10 10:21:25 2010 +0200
@@ -4829,7 +4829,7 @@
   (Haskell -)
 
 code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
 
 code_reserved SML
   list
diff -r 436554f1beaa -r 0b61951d2682 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/Option.thy	Fri Sep 10 10:21:25 2010 +0200
@@ -128,7 +128,7 @@
   (Haskell -)
 
 code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
 
 code_reserved SML
   option NONE SOME
diff -r 436554f1beaa -r 0b61951d2682 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/Product_Type.thy	Fri Sep 10 10:21:25 2010 +0200
@@ -29,7 +29,7 @@
   by (simp_all add: equal)
 
 code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
 
 code_instance bool :: equal
   (Haskell -)
@@ -110,7 +110,7 @@
   (Haskell -)
 
 code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
 
 code_reserved SML
   unit
@@ -281,7 +281,7 @@
   (Haskell -)
 
 code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
 
 types_code
   "prod"     ("(_ */ _)")
diff -r 436554f1beaa -r 0b61951d2682 src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/String.thy	Fri Sep 10 10:21:25 2010 +0200
@@ -207,7 +207,7 @@
 code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   (SML "!((_ : string) = _)")
   (OCaml "!((_ : string) = _)")
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
   (Scala infixl 5 "==")
 
 types_code
diff -r 436554f1beaa -r 0b61951d2682 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/ex/Numeral.thy	Fri Sep 10 10:21:25 2010 +0200
@@ -1086,7 +1086,7 @@
 code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
-  (Haskell infixl 4 "==")
+  (Haskell infix 4 "==")
   (Scala infixl 5 "==")
   (Eval infixl 6 "=")