# HG changeset patch
# User wenzelm
# Date 1564418679 -7200
# Node ID 52435af442a66890ff9f0ba818376e7d032987d9
# Parent  4abd07cd034f41750c269ce3b3c66bd306cd6284# Parent  03cfef16ddb4551080f8d546fa65a7a92cbb177d
merged

diff -r 03cfef16ddb4 -r 52435af442a6 NEWS
--- a/NEWS	Mon Jul 29 18:16:51 2019 +0200
+++ b/NEWS	Mon Jul 29 18:44:39 2019 +0200
@@ -23,6 +23,9 @@
 existing collections algebra_simps or field_simps to obtain
 reasonable simplification.  INCOMPATIBILITY.
 
+* Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=) associates
+to the left now as is customary.
+
 
 New in Isabelle2019 (June 2019)
 -------------------------------
@@ -3187,9 +3190,9 @@
 performance.
 
 * Property values in etc/symbols may contain spaces, if written with the
-replacement character "␣" (Unicode point 0x2324). For example:
-
-    \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
+replacement character "?" (Unicode point 0x2324). For example:
+
+    \<star>  code: 0x0022c6  group: operator  font: Deja?Vu?Sans?Mono
 
 * Java runtime environment for x86_64-windows allows to use larger heap
 space.
diff -r 03cfef16ddb4 -r 52435af442a6 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Mon Jul 29 18:16:51 2019 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Mon Jul 29 18:44:39 2019 +0200
@@ -10,27 +10,26 @@
 begin
 
 text \<open>
-  We provide a convenient do-notation for monadic expressions
-  well-known from Haskell.  \<^const>\<open>Let\<close> is printed
-  specially in do-expressions.
+We provide a convenient do-notation for monadic expressions well-known from Haskell.
+const>\<open>Let\<close> is printed specially in do-expressions.
 \<close>
 
 consts
-  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<bind>" 54)
+  bind :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd" (infixl "\<bind>" 54)
 
 notation (ASCII)
-  bind (infixr ">>=" 54)
+  bind (infixl ">>=" 54)
 
 
 abbreviation (do_notation)
-  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
+  bind_do :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd"
   where "bind_do \<equiv> bind"
 
 notation (output)
-  bind_do (infixr "\<bind>" 54)
+  bind_do (infixl "\<bind>" 54)
 
 notation (ASCII output)
-  bind_do (infixr ">>=" 54)
+  bind_do (infixl ">>=" 54)
 
 
 nonterminal do_binds and do_bind
@@ -41,11 +40,11 @@
   "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
   "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
   "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl "\<then>" 54)
 
 syntax (ASCII)
   "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
 
 translations
   "_do_block (_do_cons (_do_then t) (_do_final e))"