# HG changeset patch
# User nipkow
# Date 1564403310 -7200
# Node ID 2137db107788ef0c7b176771cb477e1b36e6bcf9
# Parent  495881aadbff5f5181e48102f180f2c9e14c24b0
Monadic bind is now infixl as is the norm

diff -r 495881aadbff -r 2137db107788 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Sun Jul 28 15:39:30 2019 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Mon Jul 29 14:28:30 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))"