diff -r 2cd7e5518d0d -r 4d9349989d94 src/HOL/Library/Multiset_Order.thy --- a/src/HOL/Library/Multiset_Order.thy Tue May 23 20:11:15 2023 +0200 +++ b/src/HOL/Library/Multiset_Order.thy Tue May 23 21:43:36 2023 +0200 @@ -776,14 +776,14 @@ "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") = - \fn phi => Cancel_Simprocs.less_cancel\ + \K Cancel_Simprocs.less_cancel\ 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" | "replicate_mset p a \ n" | "m \ replicate_mset p a" | "repeat_mset p m \ n" | "m \ repeat_mset p n") = - \fn phi => Cancel_Simprocs.less_eq_cancel\ + \K Cancel_Simprocs.less_eq_cancel\ subsection \Additional facts and instantiations\