more markup for syntax consts;
authorwenzelm
Wed, 28 Aug 2024 16:46:33 +0200
changeset 80783 14ed085de388
parent 80782 32247ad40647
child 80784 3d9e7746d9db
more markup for syntax consts;
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)"