# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1486998233 -3600
# Node ID 2b8583507891b17371195c1892c938fda057a7d4
# Parent  49c537d8789646d24c8dfcb7b84353b6b72d9066
renaming multiset simprocs

diff -r 49c537d87896 -r 2b8583507891 NEWS
--- a/NEWS	Sat Feb 11 22:53:35 2017 +0100
+++ b/NEWS	Mon Feb 13 16:03:53 2017 +0100
@@ -94,6 +94,14 @@
 * The theorem in Permutations has been renamed:
   bij_swap_ompose_bij ~> bij_swap_compose_bij
 
+* Session HOL-Library: The simprocs on subsets operators of multisets have been renamed:
+  msetless_cancel_numerals ~> msetsubset_cancel
+  msetle_cancel_numerals ~> msetsubset_eq_cancel
+INCOMPATIBILITY.
+
+* Session HOL-Library: The suffix _numerals has been removed from the name of the simprocs on multisets.
+INCOMPATIBILITY.
+
 
 *** System ***
 
diff -r 49c537d87896 -r 2b8583507891 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Feb 11 22:53:35 2017 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Feb 13 16:03:53 2017 +0100
@@ -975,28 +975,28 @@
 ML_file "multiset_simprocs_util.ML"
 ML_file "multiset_simprocs.ML"
 
-simproc_setup mseteq_cancel_numerals
+simproc_setup mseteq_cancel
   ("(l::'a multiset) + m = n" | "(l::'a multiset) = m + 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 m") =
   \<open>fn phi => Multiset_Simprocs.eq_cancel_msets\<close>
 
-simproc_setup msetless_cancel_numerals
+simproc_setup msetsubset_cancel
   ("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
    "add_mset a m \<subset># n" | "m \<subset># add_mset a n" |
    "replicate_mset p r \<subset># n" | "m \<subset># replicate_mset p r" |
    "repeat_mset p m \<subset># n" | "m \<subset># repeat_mset p m") =
   \<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close>
 
-simproc_setup msetle_cancel_numerals
+simproc_setup msetsubset_eq_cancel
   ("(l::'a multiset) + m \<subseteq># n" | "(l::'a multiset) \<subseteq># m + n" |
    "add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n" |
    "replicate_mset p r \<subseteq># n" | "m \<subseteq># replicate_mset p r" |
    "repeat_mset p m \<subseteq># n" | "m \<subseteq># repeat_mset p m") =
   \<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close>
 
-simproc_setup msetdiff_cancel_numerals
+simproc_setup msetdiff_cancel
   ("((l::'a multiset) + m) - n" | "(l::'a multiset) - (m + n)" |
    "add_mset a m - n" | "m - add_mset a n" |
    "replicate_mset p r - n" | "m - replicate_mset p r" |
diff -r 49c537d87896 -r 2b8583507891 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Sat Feb 11 22:53:35 2017 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Mon Feb 13 16:03:53 2017 +0100
@@ -261,12 +261,12 @@
 
 ML_file "multiset_order_simprocs.ML"
 
-simproc_setup msetless_cancel_numerals
+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") =
   \<open>fn phi => Multiset_Order_Simprocs.less_cancel_msets\<close>
 
-simproc_setup msetle_cancel_numerals
+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") =
   \<open>fn phi => Multiset_Order_Simprocs.le_cancel_msets\<close>