src/HOL/Library/Monad_Syntax.thy
changeset 37816 e550439d4422
parent 37791 0d6b64060543
child 37818 dd65033fed78
     1.1 --- a/src/HOL/Library/Monad_Syntax.thy	Wed Jul 14 12:27:43 2010 +0200
     1.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Wed Jul 14 12:27:44 2010 +0200
     1.3 @@ -15,21 +15,21 @@
     1.4  *}
     1.5  
     1.6  consts
     1.7 -  bindM :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
     1.8 +  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
     1.9  
    1.10  notation (xsymbols)
    1.11 -  bindM (infixr "\<guillemotright>=" 54)
    1.12 +  bind (infixr "\<guillemotright>=" 54)
    1.13  
    1.14  abbreviation (do_notation)
    1.15 -  bindM_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
    1.16 +  bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
    1.17  where
    1.18 -  "bindM_do \<equiv> bindM"
    1.19 +  "bind_do \<equiv> bind"
    1.20  
    1.21  notation (output)
    1.22 -  bindM_do (infixr ">>=" 54)
    1.23 +  bind_do (infixr ">>=" 54)
    1.24  
    1.25  notation (xsymbols output)
    1.26 -  bindM_do (infixr "\<guillemotright>=" 54)
    1.27 +  bind_do (infixr "\<guillemotright>=" 54)
    1.28  
    1.29  nonterminals
    1.30    do_binds do_bind
    1.31 @@ -49,9 +49,9 @@
    1.32  
    1.33  translations
    1.34    "_do_block (_do_cons (_do_then t) (_do_final e))"
    1.35 -    == "CONST bindM_do t (\<lambda>_. e)"
    1.36 +    == "CONST bind_do t (\<lambda>_. e)"
    1.37    "_do_block (_do_cons (_do_bind p t) (_do_final e))"
    1.38 -    == "CONST bindM_do t (\<lambda>p. e)"
    1.39 +    == "CONST bind_do t (\<lambda>p. e)"
    1.40    "_do_block (_do_cons (_do_let p t) bs)"
    1.41      == "let p = t in _do_block bs"
    1.42    "_do_block (_do_cons b (_do_cons c cs))"
    1.43 @@ -61,6 +61,9 @@
    1.44    "_do_block (_do_final e)" => "e"
    1.45    "(m >> n)" => "(m >>= (\<lambda>_. n))"
    1.46  
    1.47 -setup {* Adhoc_Overloading.add_overloaded @{const_name bindM} *}
    1.48 +setup {*
    1.49 +  Adhoc_Overloading.add_overloaded @{const_name bind}
    1.50 +  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
    1.51 +*}
    1.52  
    1.53  end