--- a/src/HOL/Library/Monad_Syntax.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy Fri Sep 20 19:51:08 2024 +0200
@@ -15,10 +15,10 @@
\<close>
consts
- bind :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd" (infixl "\<bind>" 54)
+ bind :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd" (infixl \<open>\<bind>\<close> 54)
notation (ASCII)
- bind (infixl ">>=" 54)
+ bind (infixl \<open>>>=\<close> 54)
abbreviation (do_notation)
@@ -26,25 +26,25 @@
where "bind_do \<equiv> bind"
notation (output)
- bind_do (infixl "\<bind>" 54)
+ bind_do (infixl \<open>\<bind>\<close> 54)
notation (ASCII output)
- bind_do (infixl ">>=" 54)
+ bind_do (infixl \<open>>>=\<close> 54)
nonterminal do_binds and do_bind
syntax
- "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2 _)//}" [12] 62)
- "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
- "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
- "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
- "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
- "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
- "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl "\<then>" 54)
+ "_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)
syntax (ASCII)
- "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
- "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
+ "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" (\<open>(2_ <-/ _)\<close> 13)
+ "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl \<open>>>\<close> 54)
syntax_consts
"_do_block" "_do_cons" "_do_bind" "_do_then" \<rightleftharpoons> bind and