# HG changeset patch
# User huffman
# Date 1121186672 -7200
# Node ID ac1dc3d4746ad19d43aead4fe9378a7856571aa5
# Parent  2162c0de467376ec0a4366c9aa59426cc3850d03
changed orientation of bind_assoc rule

diff -r 2162c0de4673 -r ac1dc3d4746a src/HOLCF/Fixrec.thy
--- 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 *}