# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1473661439 -7200
# Node ID 0dd6731060d72297d21f0e1d0f7d94a170dee024
# Parent  c948738d31aa49dbcda042a6d3dfe73a78547c08
delete looping simp rule

diff -r c948738d31aa -r 0dd6731060d7 src/HOL/Library/Multiset.thy
--- 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>