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
```