| changeset 20503 | 503ac4c5ef91 |
| parent 19582 | a669c98b9c24 |
| child 20770 | 2c583720436e |
--- a/src/HOL/Library/Multiset.thy Mon Sep 11 14:35:30 2006 +0200 +++ b/src/HOL/Library/Multiset.thy Mon Sep 11 21:35:19 2006 +0200 @@ -746,7 +746,7 @@ lemma multiset_of_append [simp]: "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys" - by (induct xs fixing: ys) (auto simp: union_ac) + by (induct xs arbitrary: ys) (auto simp: union_ac) lemma surj_multiset_of: "surj multiset_of" apply (unfold surj_def, rule allI)