# HG changeset patch
# User haftmann
# Date 1281529172 -7200
# Node ID 8b8fc27c1872c94c9bfb07d32d9a0cbff7554a94
# Parent  d6afb77b0f6daee82c1451a49e2bce0fa0a95d50
print fcomp combinator only monadic in connection with other monadic expressions

diff -r d6afb77b0f6d -r 8b8fc27c1872 src/HOL/Library/State_Monad.thy
--- 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))"