--- a/src/HOL/Library/Multiset.thy Tue May 31 13:02:44 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Jun 01 13:48:34 2016 +0200
@@ -90,6 +90,15 @@
end
+context
+begin
+
+qualified definition is_empty :: "'a multiset \<Rightarrow> bool" where
+ [code_abbrev]: "is_empty A \<longleftrightarrow> A = {#}"
+
+end
+
+
lift_definition single :: "'a \<Rightarrow> 'a multiset" is "\<lambda>a b. if b = a then 1 else 0"
by (rule only1_in_multiset)
@@ -2583,6 +2592,9 @@
lemma [code]: "{#} = mset []"
by simp
+lemma [code]: "Multiset.is_empty (mset xs) \<longleftrightarrow> List.null xs"
+ by (simp add: Multiset.is_empty_def List.null_def)
+
lemma [code]: "{#x#} = mset [x]"
by simp