Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorhaftmann
Wed, 11 Aug 2010 14:20:34 +0200
changeset 38346 8f32f4752288
parent 38345 8b8fc27c1872 (diff)
parent 38344 36f179131633 (current diff)
child 38347 19000bb11ff5
merged
--- a/src/HOL/Library/State_Monad.thy	Wed Aug 11 14:19:52 2010 +0200
+++ b/src/HOL/Library/State_Monad.thy	Wed Aug 11 14:20:34 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