--- a/src/HOL/Library/Multiset.thy Sun May 09 16:39:29 2004 +0200
+++ b/src/HOL/Library/Multiset.thy Sun May 09 23:04:36 2004 +0200
@@ -109,11 +109,12 @@
theorems union_ac = union_assoc union_commute union_lcomm
instance multiset :: (type) plus_ac0
- apply intro_classes
- apply (rule union_commute)
- apply (rule union_assoc)
- apply simp
- done
+proof
+ fix a b c :: "'a multiset"
+ show "(a + b) + c = a + (b + c)" by (rule union_assoc)
+ show "a + b = b + a" by (rule union_commute)
+ show "0 + a = a" by simp
+qed
subsubsection {* Difference *}