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