Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorpaulson
Thu, 03 Aug 2017 23:06:36 +0200
changeset 66321 ea6cbb69dda2
parent 66313 604616b627f2 (diff)
parent 66320 9786b06c7b5a (current diff)
child 66322 bdf4d5408b01
merged
--- 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 -
isabelle