changeset 26266 35ae83ca190a parent 26260 23ce0d32de11 child 26588 d83271bfaba5
     1.1 --- a/src/HOL/Library/State_Monad.thy	Wed Mar 12 19:38:14 2008 +0100
1.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Mar 14 08:52:51 2008 +0100
1.3 @@ -29,37 +29,29 @@
1.4
1.5  subsection {* State transformations and combinators *}
1.6
1.7 -(*<*)
1.8 -typedecl \<alpha>
1.9 -typedecl \<beta>
1.10 -typedecl \<gamma>
1.11 -typedecl \<sigma>
1.12 -typedecl \<sigma>'
1.13 -(*>*)
1.14 -
1.15  text {*
1.16    We classify functions operating on states into two categories:
1.17
1.18    \begin{description}
1.19      \item[transformations]
1.20 -      with type signature @{typ "\<sigma> \<Rightarrow> \<sigma>'"},
1.21 +      with type signature @{text "\<sigma> \<Rightarrow> \<sigma>'"},
1.22        transforming a state.
1.23      \item[yielding'' transformations]
1.24 -      with type signature @{typ "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
1.25 +      with type signature @{text "\<sigma> \<Rightarrow> \<alpha> \<times> \<sigma>'"},
1.26        yielding'' a side result while transforming a state.
1.27      \item[queries]
1.28 -      with type signature @{typ "\<sigma> \<Rightarrow> \<alpha>"},
1.29 +      with type signature @{text "\<sigma> \<Rightarrow> \<alpha>"},
1.30        computing a result dependent on a state.
1.31    \end{description}
1.32
1.33 -  By convention we write @{typ "\<sigma>"} for types representing states
1.34 -  and @{typ "\<alpha>"}, @{typ "\<beta>"}, @{typ "\<gamma>"}, @{text "\<dots>"}
1.35 +  By convention we write @{text "\<sigma>"} for types representing states
1.36 +  and @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"}
1.37    for types representing side results.  Type changes due
1.38    to transformations are not excluded in our scenario.
1.39
1.40 -  We aim to assert that values of any state type @{typ "\<sigma>"}
1.41 +  We aim to assert that values of any state type @{text "\<sigma>"}
1.42    are used in a single-threaded way: after application
1.43 -  of a transformation on a value of type @{typ "\<sigma>"}, the
1.44 +  of a transformation on a value of type @{text "\<sigma>"}, the
1.45    former value should not be used again.  To achieve this,
1.46    we use a set of monad combinators:
1.47  *}