renaming multiset simprocs
authorfleury <Mathias.Fleury@mpi-inf.mpg.de>
Mon Feb 13 16:03:53 2017 +0100 (2017-02-13)
changeset 650272b8583507891
parent 65026 49c537d87896
child 65028 87e003397834
renaming multiset simprocs
NEWS
src/HOL/Library/Multiset.thy
src/HOL/Library/Multiset_Order.thy
     1.1 --- a/NEWS	Sat Feb 11 22:53:35 2017 +0100
     1.2 +++ b/NEWS	Mon Feb 13 16:03:53 2017 +0100
     1.3 @@ -94,6 +94,14 @@
     1.4  * The theorem in Permutations has been renamed:
     1.5    bij_swap_ompose_bij ~> bij_swap_compose_bij
     1.6  
     1.7 +* Session HOL-Library: The simprocs on subsets operators of multisets have been renamed:
     1.8 +  msetless_cancel_numerals ~> msetsubset_cancel
     1.9 +  msetle_cancel_numerals ~> msetsubset_eq_cancel
    1.10 +INCOMPATIBILITY.
    1.11 +
    1.12 +* Session HOL-Library: The suffix _numerals has been removed from the name of the simprocs on multisets.
    1.13 +INCOMPATIBILITY.
    1.14 +
    1.15  
    1.16  *** System ***
    1.17  
     2.1 --- a/src/HOL/Library/Multiset.thy	Sat Feb 11 22:53:35 2017 +0100
     2.2 +++ b/src/HOL/Library/Multiset.thy	Mon Feb 13 16:03:53 2017 +0100
     2.3 @@ -975,28 +975,28 @@
     2.4  ML_file "multiset_simprocs_util.ML"
     2.5  ML_file "multiset_simprocs.ML"
     2.6  
     2.7 -simproc_setup mseteq_cancel_numerals
     2.8 +simproc_setup mseteq_cancel
     2.9    ("(l::'a multiset) + m = n" | "(l::'a multiset) = m + n" |
    2.10     "add_mset a m = n" | "m = add_mset a n" |
    2.11     "replicate_mset p a = n" | "m = replicate_mset p a" |
    2.12     "repeat_mset p m = n" | "m = repeat_mset p m") =
    2.13    \<open>fn phi => Multiset_Simprocs.eq_cancel_msets\<close>
    2.14  
    2.15 -simproc_setup msetless_cancel_numerals
    2.16 +simproc_setup msetsubset_cancel
    2.17    ("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
    2.18     "add_mset a m \<subset># n" | "m \<subset># add_mset a n" |
    2.19     "replicate_mset p r \<subset># n" | "m \<subset># replicate_mset p r" |
    2.20     "repeat_mset p m \<subset># n" | "m \<subset># repeat_mset p m") =
    2.21    \<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close>
    2.22  
    2.23 -simproc_setup msetle_cancel_numerals
    2.24 +simproc_setup msetsubset_eq_cancel
    2.25    ("(l::'a multiset) + m \<subseteq># n" | "(l::'a multiset) \<subseteq># m + n" |
    2.26     "add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n" |
    2.27     "replicate_mset p r \<subseteq># n" | "m \<subseteq># replicate_mset p r" |
    2.28     "repeat_mset p m \<subseteq># n" | "m \<subseteq># repeat_mset p m") =
    2.29    \<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close>
    2.30  
    2.31 -simproc_setup msetdiff_cancel_numerals
    2.32 +simproc_setup msetdiff_cancel
    2.33    ("((l::'a multiset) + m) - n" | "(l::'a multiset) - (m + n)" |
    2.34     "add_mset a m - n" | "m - add_mset a n" |
    2.35     "replicate_mset p r - n" | "m - replicate_mset p r" |
     3.1 --- a/src/HOL/Library/Multiset_Order.thy	Sat Feb 11 22:53:35 2017 +0100
     3.2 +++ b/src/HOL/Library/Multiset_Order.thy	Mon Feb 13 16:03:53 2017 +0100
     3.3 @@ -261,12 +261,12 @@
     3.4  
     3.5  ML_file "multiset_order_simprocs.ML"
     3.6  
     3.7 -simproc_setup msetless_cancel_numerals
     3.8 +simproc_setup msetless_cancel
     3.9    ("(l::'a::preorder multiset) + m < n" | "(l::'a multiset) < m + n" |
    3.10     "add_mset a m < n" | "m < add_mset a n") =
    3.11    \<open>fn phi => Multiset_Order_Simprocs.less_cancel_msets\<close>
    3.12  
    3.13 -simproc_setup msetle_cancel_numerals
    3.14 +simproc_setup msetle_cancel
    3.15    ("(l::'a::preorder multiset) + m \<le> n" | "(l::'a multiset) \<le> m + n" |
    3.16     "add_mset a m \<le> n" | "m \<le> add_mset a n") =
    3.17    \<open>fn phi => Multiset_Order_Simprocs.le_cancel_msets\<close>