--- a/src/HOL/Library/Multiset.thy Mon Sep 12 00:11:30 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Sep 12 08:23:59 2016 +0200
@@ -935,10 +935,6 @@
"repeat_mset n (A + B) = repeat_mset n A + repeat_mset n B"
by (auto simp: multiset_eq_iff add_mult_distrib2)
-lemma repeat_mset_distrib_add_mset [simp]:
- "repeat_mset n (add_mset a A) = repeat_mset n {#a#} + repeat_mset n A"
- by (auto simp: multiset_eq_iff)
-
ML_file "multiset_simprocs_util.ML"
ML_file "multiset_simprocs.ML"
@@ -2004,6 +2000,14 @@
m = 0 \<and> n = 0 \<or> m = n \<and> a = b"
by (auto simp add: multiset_eq_iff)
+lemma repeat_mset_replicate_mset[simp]:
+ "repeat_mset n {#a#} = replicate_mset n a"
+ by (auto simp: multiset_eq_iff)
+
+lemma repeat_mset_distrib_add_mset[simp]:
+ "repeat_mset n (add_mset a A) = replicate_mset n a + repeat_mset n A"
+ by (auto simp: multiset_eq_iff)
+
subsection \<open>Big operators\<close>