src/HOL/Library/Multiset.thy
changeset 27611 2c01c0bdb385
parent 27487 c8a6ce181805
child 27682 25aceefd4786
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Jul 15 16:02:10 2008 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Jul 15 16:50:09 2008 +0200
     1.3 @@ -1421,9 +1421,12 @@
     1.4  qed
     1.5  
     1.6  lemma fold_mset_fusion:
     1.7 -  includes left_commutative g
     1.8 -  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A"
     1.9 -by (induct A) auto
    1.10 +  assumes "left_commutative g"
    1.11 +  shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
    1.12 +proof -
    1.13 +  interpret left_commutative [g] by fact
    1.14 +  show "PROP ?P" by (induct A) auto
    1.15 +qed
    1.16  
    1.17  lemma fold_mset_rec:
    1.18    assumes "a \<in># A"