author | paulson |
Thu, 03 Aug 2017 23:06:36 +0200 | |
changeset 66321 | ea6cbb69dda2 |
parent 66313 | 604616b627f2 (diff) |
parent 66320 | 9786b06c7b5a (current diff) |
child 66322 | bdf4d5408b01 |
--- a/src/HOL/Library/Multiset.thy Thu Aug 03 21:38:05 2017 +0200 +++ b/src/HOL/Library/Multiset.thy Thu Aug 03 23:06:36 2017 +0200 @@ -3458,8 +3458,7 @@ end -lemma [code]: "sum_mset (mset xs) = sum_list xs" - by (induct xs) simp_all +declare sum_mset_sum_list [code] lemma [code]: "prod_mset (mset xs) = fold times xs 1" proof -