diff -r 5280c02f29dc -r c5059f9fbfba src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Nov 26 19:44:21 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Nov 26 11:14:10 2021 +0100
@@ -2798,6 +2798,9 @@
 definition mult :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
   "mult r = (mult1 r)\<^sup>+"
 
+definition multp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  "multp r M N \<longleftrightarrow> (M, N) \<in> mult {(x, y). r x y}"
+
 lemma mult1I:
   assumes "M = add_mset a M0" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
   shows "(N, M) \<in> mult1 r"
@@ -2810,14 +2813,14 @@
 
 lemma mono_mult1:
   assumes "r \<subseteq> r'" shows "mult1 r \<subseteq> mult1 r'"
-unfolding mult1_def using assms by blast
+  unfolding mult1_def using assms by blast
 
 lemma mono_mult:
   assumes "r \<subseteq> r'" shows "mult r \<subseteq> mult r'"
-unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+  unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
 
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
-by (simp add: mult1_def)
+  by (simp add: mult1_def)
 
 lemma less_add:
   assumes mult1: "(N, add_mset a M0) \<in> mult1 r"