src/HOL/Library/State_Monad.thy
changeset 37751 89e16802b6cc
parent 35115 446c5063e4fd
child 37791 0d6b64060543
     1.1 --- a/src/HOL/Library/State_Monad.thy	Thu Jul 08 17:23:05 2010 +0200
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Jul 09 08:11:10 2010 +0200
     1.3 @@ -55,23 +55,23 @@
     1.4    we use a set of monad combinators:
     1.5  *}
     1.6  
     1.7 -notation fcomp (infixl "o>" 60)
     1.8 -notation (xsymbols) fcomp (infixl "o>" 60)
     1.9 +notation fcomp (infixl "\<circ>>" 60)
    1.10 +notation (xsymbols) fcomp (infixl "\<circ>>" 60)
    1.11  notation scomp (infixl "o->" 60)
    1.12 -notation (xsymbols) scomp (infixl "o\<rightarrow>" 60)
    1.13 +notation (xsymbols) scomp (infixl "\<circ>\<rightarrow>" 60)
    1.14  
    1.15  abbreviation (input)
    1.16    "return \<equiv> Pair"
    1.17  
    1.18  text {*
    1.19    Given two transformations @{term f} and @{term g}, they
    1.20 -  may be directly composed using the @{term "op o>"} combinator,
    1.21 -  forming a forward composition: @{prop "(f o> g) s = f (g s)"}.
    1.22 +  may be directly composed using the @{term "op \<circ>>"} combinator,
    1.23 +  forming a forward composition: @{prop "(f \<circ>> g) s = f (g s)"}.
    1.24  
    1.25    After any yielding transformation, we bind the side result
    1.26    immediately using a lambda abstraction.  This 
    1.27 -  is the purpose of the @{term "op o\<rightarrow>"} combinator:
    1.28 -  @{prop "(f o\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
    1.29 +  is the purpose of the @{term "op \<circ>\<rightarrow>"} combinator:
    1.30 +  @{prop "(f \<circ>\<rightarrow> (\<lambda>x. g)) s = (let (x, s') = f s in g s')"}.
    1.31  
    1.32    For queries, the existing @{term "Let"} is appropriate.
    1.33  
    1.34 @@ -141,8 +141,8 @@
    1.35  
    1.36  translations
    1.37    "_do f" => "f"
    1.38 -  "_scomp x f g" => "f o\<rightarrow> (\<lambda>x. g)"
    1.39 -  "_fcomp f g" => "f o> g"
    1.40 +  "_scomp x f g" => "f \<circ>\<rightarrow> (\<lambda>x. g)"
    1.41 +  "_fcomp f g" => "f \<circ>> g"
    1.42    "_let x t f" => "CONST Let t (\<lambda>x. f)"
    1.43    "_done f" => "f"
    1.44