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.
print fcomp combinator only monadic in connection with other monadic expressions
authorhaftmann
Wed, 11 Aug 2010 14:19:32 +0200
changeset 38345 8b8fc27c1872
parent 38327 d6afb77b0f6d
child 38346 8f32f4752288
print fcomp combinator only monadic in connection with other monadic expressions
src/HOL/Library/State_Monad.thy file | annotate | diff | comparison | revisions 
--- 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