lemma is_empty_empty

--- a/src/HOL/Library/Mapping.thy	Sun Apr 11 16:51:05 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Sun Apr 11 16:51:06 2010 +0200
@@ -122,6 +122,10 @@
   "bulkload xs = tabulate [0..<length xs] (nth xs)"
   by (rule mapping_eqI) (simp add: expand_fun_eq)
 
+lemma is_empty_empty:
+  "is_empty m \<longleftrightarrow> m = Mapping Map.empty"
+  by (cases m) (simp add: is_empty_def)
+
 
 subsection {* Some technical code lemmas *}