--- a/src/HOL/Library/Multiset.thy Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Fri May 13 20:24:10 2016 +0200
@@ -967,7 +967,7 @@
lemma multiset_cases [cases type]:
obtains (empty) "M = {#}"
| (add) N x where "M = N + {#x#}"
- using assms by (induct M) simp_all
+ by (induct M) simp_all
lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
by (cases "B = {#}") (auto dest: multi_member_split)
@@ -1455,7 +1455,7 @@
by (induct n, simp_all)
lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<subseteq># M"
- by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
+ by (auto simp add: mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
by (induct D) simp_all