equal
deleted
inserted
replaced
117 |
117 |
118 subsection \<open>Do-syntax\<close> |
118 subsection \<open>Do-syntax\<close> |
119 |
119 |
120 nonterminal sdo_binds and sdo_bind |
120 nonterminal sdo_binds and sdo_bind |
121 |
121 |
122 definition sdo_syntax :: 'a |
122 definition "sdo_syntax = ()" |
123 where "sdo_syntax = undefined" |
|
124 |
123 |
125 syntax |
124 syntax |
126 "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2 _)//}" [12] 62) |
125 "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2 _)//}" [12] 62) |
127 "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13) |
126 "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13) |
128 "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13) |
127 "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13) |