1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Less_Monad_Syntax (* use instead of HOL-Library.Monad_Syntax *)
8  imports "HOL-Library.Monad_Syntax"
9begin
10
11(* remove >> from Monad_Syntax, clashes with word shift *)
12no_syntax
13  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
14
15(* remove input version of >>= from Monad_Syntax, avoid clash with NonDetMonad *)
16no_notation
17  Monad_Syntax.bind (infixl ">>=" 54)
18
19(* use ASCII >>= instead of \<bind> *)
20notation (output)
21  bind_do (infixl ">>=" 54)
22
23(* enable pretty printing for do { .. } syntax globally *)
24translations
25  "CONST bind_do" <= "CONST bind"
26
27end
28