src/HOL/Library/Monad_Syntax.thy
changeset 61955 e96292f32c3c
parent 60500 903bb1495239
child 62026 ea3b1b0413b4
     1.1 --- a/src/HOL/Library/Monad_Syntax.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -15,42 +15,42 @@
     1.4  \<close>
     1.5  
     1.6  consts
     1.7 -  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr ">>=" 54)
     1.8 +  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<guillemotright>=" 54)
     1.9  
    1.10 -notation (xsymbols)
    1.11 -  bind (infixr "\<guillemotright>=" 54)
    1.12 +notation (ASCII)
    1.13 +  bind (infixr ">>=" 54)
    1.14  
    1.15  notation (latex output)
    1.16    bind (infixr "\<bind>" 54)
    1.17  
    1.18 +
    1.19  abbreviation (do_notation)
    1.20    bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
    1.21 -where
    1.22 -  "bind_do \<equiv> bind"
    1.23 +  where "bind_do \<equiv> bind"
    1.24  
    1.25  notation (output)
    1.26 -  bind_do (infixr ">>=" 54)
    1.27 +  bind_do (infixr "\<guillemotright>=" 54)
    1.28  
    1.29 -notation (xsymbols output)
    1.30 -  bind_do (infixr "\<guillemotright>=" 54)
    1.31 +notation (ASCII output)
    1.32 +  bind_do (infixr ">>=" 54)
    1.33  
    1.34  notation (latex output)
    1.35    bind_do (infixr "\<bind>" 54)
    1.36  
    1.37 +
    1.38  nonterminal do_binds and do_bind
    1.39 -
    1.40  syntax
    1.41    "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
    1.42 -  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
    1.43 +  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
    1.44    "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
    1.45    "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
    1.46    "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
    1.47    "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
    1.48 -  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
    1.49 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
    1.50  
    1.51 -syntax (xsymbols)
    1.52 -  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
    1.53 -  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
    1.54 +syntax (ASCII)
    1.55 +  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
    1.56 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
    1.57  
    1.58  syntax (latex output)
    1.59    "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)