src/HOL/Library/Multiset.thy
changeset 14722 8e739a6eaf11
parent 14706 71590b7733b7
child 14738 83f1a514dcb4
     1.1 --- a/src/HOL/Library/Multiset.thy	Sun May 09 16:39:29 2004 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sun May 09 23:04:36 2004 +0200
     1.3 @@ -109,11 +109,12 @@
     1.4  theorems union_ac = union_assoc union_commute union_lcomm
     1.5  
     1.6  instance multiset :: (type) plus_ac0
     1.7 -  apply intro_classes
     1.8 -    apply (rule union_commute)
     1.9 -   apply (rule union_assoc)
    1.10 -  apply simp
    1.11 -  done
    1.12 +proof 
    1.13 +  fix a b c :: "'a multiset"
    1.14 +  show "(a + b) + c = a + (b + c)" by (rule union_assoc)
    1.15 +  show "a + b = b + a" by (rule union_commute)
    1.16 +  show "0 + a = a" by simp
    1.17 +qed
    1.18  
    1.19  
    1.20  subsubsection {* Difference *}