# HG changeset patch # User wenzelm # Date 1724866807 -7200 # Node ID 3d9e7746d9dbdcfff0814bf927cccb139d41b9c4 # Parent 14ed085de3886c7ec5081447e0a0636f1f338fd7 further attempts at markup for monad notation; diff -r 14ed085de388 -r 3d9e7746d9db src/HOL/Library/Monad_Syntax.thy --- a/src/HOL/Library/Monad_Syntax.thy Wed Aug 28 16:46:33 2024 +0200 +++ b/src/HOL/Library/Monad_Syntax.thy Wed Aug 28 19:40:07 2024 +0200 @@ -47,8 +47,7 @@ "_thenM" :: "['a, 'b] \ 'c" (infixl ">>" 54) syntax_consts - "_do_block" "_do_cons" \ bind_do and - "_do_bind" "_thenM" \ bind and + "_do_block" "_do_cons" "_do_bind" "_do_then" \ bind and "_do_let" \ Let translations diff -r 14ed085de388 -r 3d9e7746d9db src/HOL/Library/Open_State_Syntax.thy --- 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 \ 'a" ("exec {//(2 _)//}" [12] 62) "_sdo_bind" :: "[pttrn, 'a] \ sdo_bind" ("(_ \/ _)" 13) @@ -131,8 +134,8 @@ "_sdo_bind" :: "[pttrn, 'a] \ sdo_bind" ("(_ <-/ _)" 13) syntax_consts + "_sdo_block" "_sdo_cons" == sdo_syntax and "_sdo_bind" == scomp and - "_sdo_then" == fcomp and "_sdo_let" == Let translations