--- 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