# HG changeset patch
# User wenzelm
# Date 1729259138 -7200
# Node ID c66e24eae28175dedfa1d2c2042b47a1cd16b4dc
# Parent  5036454794a53f53d0ba3544682c282088e80677
clarified inner-syntax markup;

diff -r 5036454794a5 -r c66e24eae281 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Fri Oct 18 15:42:31 2024 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Fri Oct 18 15:45:38 2024 +0200
@@ -34,17 +34,22 @@
 
 nonterminal do_binds and do_bind
 syntax
-  "_do_block" :: "do_binds \<Rightarrow> 'a" (\<open>do {//(2  _)//}\<close> [12] 62)
-  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" (\<open>(2_ \<leftarrow>/ _)\<close> 13)
-  "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" (\<open>(2let _ =/ _)\<close> [1000, 13] 13)
-  "_do_then" :: "'a \<Rightarrow> do_bind" (\<open>_\<close> [14] 13)
-  "_do_final" :: "'a \<Rightarrow> do_binds" (\<open>_\<close>)
-  "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" (\<open>_;//_\<close> [13, 12] 12)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl \<open>\<then>\<close> 54)
+  "_do_block" :: "do_binds \<Rightarrow> 'a"
+    (\<open>(\<open>open_block notation=\<open>mixfix do block\<close>\<close>do {//(2  _)//})\<close> [12] 62)
+  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind"
+    (\<open>(\<open>indent=2 notation=\<open>infix do bind\<close>\<close>_ \<leftarrow>/ _)\<close> 13)
+  "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind"
+    (\<open>(\<open>indent=2 notation=\<open>infix do let\<close>\<close>let _ =/ _)\<close> [1000, 13] 13)
+  "_do_then" :: "'a \<Rightarrow> do_bind"  (\<open>_\<close> [14] 13)
+  "_do_final" :: "'a \<Rightarrow> do_binds"  (\<open>_\<close>)
+  "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds"
+    (\<open>(\<open>open_block notation=\<open>infix do next\<close>\<close>_;//_)\<close> [13, 12] 12)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c"  (infixl \<open>\<then>\<close> 54)
 
 syntax (ASCII)
-  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" (\<open>(2_ <-/ _)\<close> 13)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl \<open>>>\<close> 54)
+  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind"
+    (\<open>(\<open>indent=2 notation=\<open>infix do bind\<close>\<close>_ <-/ _)\<close> 13)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c"  (infixl \<open>>>\<close> 54)
 
 syntax_consts
   "_do_block" "_do_cons" "_do_bind" "_do_then" \<rightleftharpoons> bind and
diff -r 5036454794a5 -r c66e24eae281 src/HOL/Library/Open_State_Syntax.thy
--- a/src/HOL/Library/Open_State_Syntax.thy	Fri Oct 18 15:42:31 2024 +0200
+++ b/src/HOL/Library/Open_State_Syntax.thy	Fri Oct 18 15:45:38 2024 +0200
@@ -119,22 +119,23 @@
 
 nonterminal sdo_binds and sdo_bind
 
-definition "sdo_syntax = ()"
-
 syntax
-  "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" (\<open>exec {//(2  _)//}\<close> [12] 62)
-  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" (\<open>(_ \<leftarrow>/ _)\<close> 13)
-  "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" (\<open>(2let _ =/ _)\<close> [1000, 13] 13)
-  "_sdo_then" :: "'a \<Rightarrow> sdo_bind" (\<open>_\<close> [14] 13)
-  "_sdo_final" :: "'a \<Rightarrow> sdo_binds" (\<open>_\<close>)
-  "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" (\<open>_;//_\<close> [13, 12] 12)
+  "_sdo_block" :: "sdo_binds \<Rightarrow> 'a"
+    (\<open>(\<open>open_block notation=\<open>mixfix exec block\<close>\<close>exec {//(2  _)//})\<close> [12] 62)
+  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind"
+    (\<open>(\<open>indent=2 notation=\<open>infix exec bind\<close>\<close>_ \<leftarrow>/ _)\<close> 13)
+  "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind"
+    (\<open>(\<open>indent=2 notation=\<open>infix exec let\<close>\<close>let _ =/ _)\<close> [1000, 13] 13)
+  "_sdo_then" :: "'a \<Rightarrow> sdo_bind"  (\<open>_\<close> [14] 13)
+  "_sdo_final" :: "'a \<Rightarrow> sdo_binds"  (\<open>_\<close>)
+  "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds"
+    (\<open>(\<open>open_block notation=\<open>infix exec next\<close>\<close>_;//_)\<close> [13, 12] 12)
 
 syntax (ASCII)
-  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" (\<open>(_ <-/ _)\<close> 13)
+  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind"
+    (\<open>(\<open>indent=2 notation=\<open>infix exec bind\<close>\<close>_ <-/ _)\<close> 13)
 
 syntax_consts
-  "_sdo_block" "_sdo_cons" == sdo_syntax and
-  "_sdo_bind" == scomp and
   "_sdo_let" == Let
 
 translations