# HG changeset patch # User haftmann # Date 1279103264 -7200 # Node ID e550439d4422d136761a073e3b4b4ce96fa6e307 # Parent 053d23f089464f5f1089fabf99997048b963a0f8 dropped M suffix; added predicate monad bind diff -r 053d23f08946 -r e550439d4422 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Jul 14 12:27:43 2010 +0200 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Jul 14 12:27:44 2010 +0200 @@ -266,10 +266,9 @@ setup {* Adhoc_Overloading.add_variant - @{const_name Monad_Syntax.bindM} @{const_name Heap_Monad.bind} + @{const_name Monad_Syntax.bind} @{const_name Heap_Monad.bind} *} - lemma execute_bind [execute_simps]: "execute f h = Some (x, h') \ execute (f \= g) h = execute (g x) h'" "execute f h = None \ execute (f \= g) h = None" diff -r 053d23f08946 -r e550439d4422 src/HOL/Library/Monad_Syntax.thy --- a/src/HOL/Library/Monad_Syntax.thy Wed Jul 14 12:27:43 2010 +0200 +++ b/src/HOL/Library/Monad_Syntax.thy Wed Jul 14 12:27:44 2010 +0200 @@ -15,21 +15,21 @@ *} consts - bindM :: "['a, 'b \ 'c] \ 'c" (infixr ">>=" 54) + bind :: "['a, 'b \ 'c] \ 'c" (infixr ">>=" 54) notation (xsymbols) - bindM (infixr "\=" 54) + bind (infixr "\=" 54) abbreviation (do_notation) - bindM_do :: "['a, 'b \ 'c] \ 'c" + bind_do :: "['a, 'b \ 'c] \ 'c" where - "bindM_do \ bindM" + "bind_do \ bind" notation (output) - bindM_do (infixr ">>=" 54) + bind_do (infixr ">>=" 54) notation (xsymbols output) - bindM_do (infixr "\=" 54) + bind_do (infixr "\=" 54) nonterminals do_binds do_bind @@ -49,9 +49,9 @@ translations "_do_block (_do_cons (_do_then t) (_do_final e))" - == "CONST bindM_do t (\_. e)" + == "CONST bind_do t (\_. e)" "_do_block (_do_cons (_do_bind p t) (_do_final e))" - == "CONST bindM_do t (\p. e)" + == "CONST bind_do t (\p. e)" "_do_block (_do_cons (_do_let p t) bs)" == "let p = t in _do_block bs" "_do_block (_do_cons b (_do_cons c cs))" @@ -61,6 +61,9 @@ "_do_block (_do_final e)" => "e" "(m >> n)" => "(m >>= (\_. n))" -setup {* Adhoc_Overloading.add_overloaded @{const_name bindM} *} +setup {* + Adhoc_Overloading.add_overloaded @{const_name bind} + #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind} +*} end