author | wenzelm |
Wed, 28 Aug 2024 16:46:33 +0200 | |
changeset 80783 | 14ed085de388 |
parent 80782 | 32247ad40647 |
child 80784 | 3d9e7746d9db |
--- 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)"