| changeset 14738 | 83f1a514dcb4 |
| parent 14722 | 8e739a6eaf11 |
| child 14981 | e73f8140af78 |
--- a/src/HOL/Library/Multiset.thy Tue May 11 14:00:02 2004 +0200 +++ b/src/HOL/Library/Multiset.thy Tue May 11 20:11:08 2004 +0200 @@ -108,7 +108,7 @@ theorems union_ac = union_assoc union_commute union_lcomm -instance multiset :: (type) plus_ac0 +instance multiset :: (type) comm_monoid_add proof fix a b c :: "'a multiset" show "(a + b) + c = a + (b + c)" by (rule union_assoc)