Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Haskell == is infix, not infixl
authorhaftmann
Fri, 10 Sep 2010 10:21:25 +0200
changeset 39272 0b61951d2682
parent 39271 436554f1beaa
child 39273 92aa2a0f7399
Haskell == is infix, not infixl
src/HOL/Code_Numeral.thy file | annotate | diff | comparison | revisions
src/HOL/HOL.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Code_Char.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Code_Integer.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Code_Natural.thy file | annotate | diff | comparison | revisions
src/HOL/Library/Efficient_Nat.thy file | annotate | diff | comparison | revisions
src/HOL/List.thy file | annotate | diff | comparison | revisions
src/HOL/Option.thy file | annotate | diff | comparison | revisions
src/HOL/Product_Type.thy file | annotate | diff | comparison | revisions
src/HOL/String.thy file | annotate | diff | comparison | revisions
src/HOL/ex/Numeral.thy file | annotate | diff | comparison | revisions 
--- 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) = _)")
 
--- 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 *}
 
--- 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"
--- 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 "=")
 
--- 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"
--- 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 "=")
 
--- 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
--- 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
--- 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"     ("(_ */ _)")
--- 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
--- 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 "=")
isabelle