src/HOL/Library/State_Monad.thy
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  *}