changeset 36635 | 080b755377c0 |
parent 35901 | 12f09bf2c77f |
child 37770 | cddb3106adb8 |
--- a/src/HOLCF/UpperPD.thy Tue May 04 08:55:39 2010 +0200 +++ b/src/HOLCF/UpperPD.thy Tue May 04 08:55:43 2010 +0200 @@ -388,7 +388,7 @@ (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)" lemma ACI_upper_bind: - "ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)" + "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f +\<sharp> y\<cdot>f)" apply unfold_locales apply (simp add: upper_plus_assoc) apply (simp add: upper_plus_commute)