equal
deleted
inserted
replaced
112 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta |
112 lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta |
113 |
113 |
114 |
114 |
115 subsection {* Do-syntax *} |
115 subsection {* Do-syntax *} |
116 |
116 |
117 nonterminals |
117 nonterminal sdo_binds and sdo_bind |
118 sdo_binds sdo_bind |
|
119 |
118 |
120 syntax |
119 syntax |
121 "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2 _)//}" [12] 62) |
120 "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2 _)//}" [12] 62) |
122 "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13) |
121 "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13) |
123 "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13) |
122 "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13) |