changeset 29244 | 95d591908d8d |
parent 29237 | e90d9d51106b |
child 29252 | ea97aa6aeba2 |
--- a/src/HOLCF/ConvexPD.thy Fri Dec 19 11:09:31 2008 +0100 +++ b/src/HOLCF/ConvexPD.thy Fri Dec 19 11:57:21 2008 +0100 @@ -296,7 +296,7 @@ apply (simp add: PDPlus_absorb) done -interpretation aci_convex_plus!: ab_semigroup_idem_mult "op +\<natural>" +class_interpretation aci_convex_plus: ab_semigroup_idem_mult ["op +\<natural>"] by unfold_locales (rule convex_plus_assoc convex_plus_commute convex_plus_absorb)+