src/HOL/Library/Monad_Syntax.thy
changeset 59359 07b9893cd8a7
parent 58881 b9556a055632
child 60500 903bb1495239
     1.1 --- a/src/HOL/Library/Monad_Syntax.thy	Wed Jan 14 13:51:34 2015 +0100
     1.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Wed Jan 14 15:22:50 2015 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  syntax
     1.6    "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
     1.7 -  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
     1.8 +  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
     1.9    "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
    1.10    "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
    1.11    "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
    1.12 @@ -49,7 +49,7 @@
    1.13    "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
    1.14  
    1.15  syntax (xsymbols)
    1.16 -  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
    1.17 +  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
    1.18    "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
    1.19  
    1.20  syntax (latex output)