src/HOL/Library/State_Monad.thy
changeset 61955 e96292f32c3c
parent 61585 a9599d3d7610
child 63362 9321740ae1d4
     1.1 --- a/src/HOL/Library/State_Monad.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -118,14 +118,14 @@
     1.4  
     1.5  syntax
     1.6    "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
     1.7 -  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
     1.8 +  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
     1.9    "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
    1.10    "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13)
    1.11    "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_")
    1.12    "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12)
    1.13  
    1.14 -syntax (xsymbols)
    1.15 -  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
    1.16 +syntax (ASCII)
    1.17 +  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
    1.18  
    1.19  translations
    1.20    "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"