diff -r 067210a08a22 -r b0f89998c2a1 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Apr 12 09:27:43 2017 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Apr 12 09:27:47 2017 +0200
@@ -503,10 +503,10 @@
 subsubsection \<open>Pointwise ordering induced by count\<close>
 
 definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
-  where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)"
+  where "A \<subseteq># B \<longleftrightarrow> (\<forall>a. count A a \<le> count B a)"
 
 definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
-  where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)"
+  where "A \<subset># B \<longleftrightarrow> A \<subseteq># B \<and> A \<noteq> B"
 
 abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<supseteq>#" 50)
   where "supseteq_mset A B \<equiv> B \<subseteq># A"