# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1486998235 -3600
# Node ID 87e003397834ef8f8c2532951d78c74470eff0d5
# Parent  2b8583507891b17371195c1892c938fda057a7d4
adding simplification patterns to multiset simprocs

diff -r 2b8583507891 -r 87e003397834 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Mon Feb 13 16:03:53 2017 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Mon Feb 13 16:03:55 2017 +0100
@@ -263,12 +263,16 @@
 
 simproc_setup msetless_cancel
   ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" |
-   "add_mset a m < n" | "m < add_mset a n") =
+   "add_mset a m < n" | "m < add_mset a n" |
+   "replicate_mset p a < n" | "m < replicate_mset p a" |
+   "repeat_mset p m < n" | "m < repeat_mset p n") =
   \<open>fn phi => Multiset_Order_Simprocs.less_cancel_msets\<close>
 
 simproc_setup msetle_cancel
   ("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" |
-   "add_mset a m \<le> n" | "m \<le> add_mset a n") =
+   "add_mset a m \<le> n" | "m \<le> add_mset a n" |
+   "replicate_mset p a \<le> n" | "m \<le> replicate_mset p a" |
+   "repeat_mset p m \<le> n" | "m \<le> repeat_mset p n") =
   \<open>fn phi => Multiset_Order_Simprocs.le_cancel_msets\<close>