changed orientation of bind_assoc rule
authorhuffman
Tue Jul 12 18:44:32 2005 +0200 (2005-07-12)
changeset 16779ac1dc3d4746a
parent 16778 2162c0de4673
child 16780 aa284c1b72ad
changed orientation of bind_assoc rule
src/HOLCF/Fixrec.thy
     1.1 --- a/src/HOLCF/Fixrec.thy	Tue Jul 12 18:28:36 2005 +0200
     1.2 +++ b/src/HOLCF/Fixrec.thy	Tue Jul 12 18:44:32 2005 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4  by (rule_tac p=m in maybeE, simp_all)
     1.5  
     1.6  lemma bind_assoc [simp]:
     1.7 - "(do a <- m; b <- k\<cdot>a; h\<cdot>b) = (do b <- (do a <- m; k\<cdot>a); h\<cdot>b)"
     1.8 + "(do b <- (do a <- m; k\<cdot>a); h\<cdot>b) = (do a <- m; b <- k\<cdot>a; h\<cdot>b)"
     1.9  by (rule_tac p=m in maybeE, simp_all)
    1.10  
    1.11  subsection {* Run operator *}