--- 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"