src/HOL/Library/State_Monad.thy
changeset 37817 71e5546b1965
parent 37791 0d6b64060543
child 37932 d00a3f47b607
     1.1 --- a/src/HOL/Library/State_Monad.thy	Wed Jul 14 12:27:44 2010 +0200
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Jul 14 12:27:44 2010 +0200
     1.3 @@ -56,9 +56,7 @@
     1.4  *}
     1.5  
     1.6  notation fcomp (infixl "\<circ>>" 60)
     1.7 -notation (xsymbols) fcomp (infixl "\<circ>>" 60)
     1.8 -notation scomp (infixl "o->" 60)
     1.9 -notation (xsymbols) scomp (infixl "\<circ>\<rightarrow>" 60)
    1.10 +notation scomp (infixl "\<circ>\<rightarrow>" 60)
    1.11  
    1.12  abbreviation (input)
    1.13    "return \<equiv> Pair"
    1.14 @@ -112,10 +110,14 @@
    1.15  
    1.16  lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
    1.17  
    1.18 +
    1.19 +subsection {* Do-syntax *}
    1.20 +
    1.21  setup {*
    1.22 -  Adhoc_Overloading.add_variant @{const_name bindM} @{const_name scomp}
    1.23 +  Adhoc_Overloading.add_variant @{const_name bind} @{const_name scomp}
    1.24  *}
    1.25  
    1.26 +
    1.27  text {*
    1.28    For an example, see HOL/Extraction/Higman.thy.
    1.29  *}