# HG changeset patch
# User wenzelm
# Date 1724856393 -7200
# Node ID 14ed085de3886c7ec5081447e0a0636f1f338fd7
# Parent  32247ad40647fb10c1442c817f614c59f5d07169
more markup for syntax consts;

diff -r 32247ad40647 -r 14ed085de388 src/HOL/Library/Open_State_Syntax.thy
--- a/src/HOL/Library/Open_State_Syntax.thy	Tue Aug 27 13:53:18 2024 +0200
+++ b/src/HOL/Library/Open_State_Syntax.thy	Wed Aug 28 16:46:33 2024 +0200
@@ -130,6 +130,11 @@
 syntax (ASCII)
   "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
 
+syntax_consts
+  "_sdo_bind" == scomp and
+  "_sdo_then" == fcomp and
+  "_sdo_let" == Let
+
 translations
   "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
     == "CONST scomp t (\<lambda>p. e)"