replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
authorobua
Sun May 09 23:04:36 2004 +0200 (2004-05-09)
changeset 147228e739a6eaf11
parent 14721 782932b1e931
child 14723 b77ce15b625a
replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
src/HOL/Library/Multiset.thy
     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 *}