src/HOL/Library/State_Monad.thy
changeset 38345 8b8fc27c1872
parent 37932 d00a3f47b607
child 40359 84388bba911d
     1.1 --- a/src/HOL/Library/State_Monad.thy	Wed Aug 11 13:39:36 2010 +0200
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Wed Aug 11 14:19:32 2010 +0200
     1.3 @@ -131,7 +131,11 @@
     1.4    "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
     1.5      == "CONST scomp t (\<lambda>p. e)"
     1.6    "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
     1.7 -    == "CONST fcomp t e"
     1.8 +    => "CONST fcomp t e"
     1.9 +  "_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))"
    1.10 +    <= "_sdo_final (CONST fcomp t e)"
    1.11 +  "_sdo_block (_sdo_cons (_sdo_then t) e)"
    1.12 +    <= "CONST fcomp t (_sdo_block e)"
    1.13    "_sdo_block (_sdo_cons (_sdo_let p t) bs)"
    1.14      == "let p = t in _sdo_block bs"
    1.15    "_sdo_block (_sdo_cons b (_sdo_cons c cs))"