Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/State_Monad.thy
changeset 38345 8b8fc27c1872
parent 37932 d00a3f47b607
child 40359 84388bba911d 
--- a/src/HOL/Library/State_Monad.thy	Wed Aug 11 13:39:36 2010 +0200
+++ b/src/HOL/Library/State_Monad.thy	Wed Aug 11 14:19:32 2010 +0200
@@ -131,7 +131,11 @@
   "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
     == "CONST scomp t (\<lambda>p. e)"
   "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
-    == "CONST fcomp t e"
+    => "CONST fcomp t e"
+  "_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))"
+    <= "_sdo_final (CONST fcomp t e)"
+  "_sdo_block (_sdo_cons (_sdo_then t) e)"
+    <= "CONST fcomp t (_sdo_block e)"
   "_sdo_block (_sdo_cons (_sdo_let p t) bs)"
     == "let p = t in _sdo_block bs"
   "_sdo_block (_sdo_cons b (_sdo_cons c cs))"
isabelle