--- a/src/HOL/Library/Monad_Syntax.thy Wed Aug 28 16:46:33 2024 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy Wed Aug 28 19:40:07 2024 +0200
@@ -47,8 +47,7 @@
"_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
syntax_consts
- "_do_block" "_do_cons" \<rightleftharpoons> bind_do and
- "_do_bind" "_thenM" \<rightleftharpoons> bind and
+ "_do_block" "_do_cons" "_do_bind" "_do_then" \<rightleftharpoons> bind and
"_do_let" \<rightleftharpoons> Let
translations
--- a/src/HOL/Library/Open_State_Syntax.thy Wed Aug 28 16:46:33 2024 +0200
+++ b/src/HOL/Library/Open_State_Syntax.thy Wed Aug 28 19:40:07 2024 +0200
@@ -119,6 +119,9 @@
nonterminal sdo_binds and sdo_bind
+definition sdo_syntax :: 'a
+ where "sdo_syntax = undefined"
+
syntax
"_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2 _)//}" [12] 62)
"_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
@@ -131,8 +134,8 @@
"_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
syntax_consts
+ "_sdo_block" "_sdo_cons" == sdo_syntax and
"_sdo_bind" == scomp and
- "_sdo_then" == fcomp and
"_sdo_let" == Let
translations