author | huffman |
Tue, 12 Jul 2005 18:44:32 +0200 | |
changeset 16779 | ac1dc3d4746a |
parent 16778 | 2162c0de4673 |
child 16780 | aa284c1b72ad |
--- a/src/HOLCF/Fixrec.thy Tue Jul 12 18:28:36 2005 +0200 +++ b/src/HOLCF/Fixrec.thy Tue Jul 12 18:44:32 2005 +0200 @@ -73,7 +73,7 @@ by (rule_tac p=m in maybeE, simp_all) lemma bind_assoc [simp]: - "(do a <- m; b <- k\<cdot>a; h\<cdot>b) = (do b <- (do a <- m; k\<cdot>a); h\<cdot>b)" + "(do b <- (do a <- m; k\<cdot>a); h\<cdot>b) = (do a <- m; b <- k\<cdot>a; h\<cdot>b)" by (rule_tac p=m in maybeE, simp_all) subsection {* Run operator *}