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") = \fn phi => Multiset_Order_Simprocs.less_cancel_msets\ -simproc_setup msetle_cancel_numerals +simproc_setup msetle_cancel ("(l::'a::preorder multiset) + m \ n" | "(l::'a multiset) \ m + n" | "add_mset a m \ n" | "m \ add_mset a n") = \fn phi => Multiset_Order_Simprocs.le_cancel_msets\