src/HOL/HOLCF/LowerPD.thy
changeset 51489 f738e6dbd844
parent 49834 b27bbb021df1
child 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/LowerPD.thy	Sat Mar 23 17:11:06 2013 +0100
     1.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Sat Mar 23 20:50:39 2013 +0100
     1.3 @@ -309,7 +309,7 @@
     1.4      (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)"
     1.5  
     1.6  lemma ACI_lower_bind:
     1.7 -  "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)"
     1.8 +  "semilattice (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<flat> y\<cdot>f)"
     1.9  apply unfold_locales
    1.10  apply (simp add: lower_plus_assoc)
    1.11  apply (simp add: lower_plus_commute)