src/HOL/Library/Mapping.thy
changeset 36110 4ab91a42666a
parent 35194 a6c573d13385
child 36176 3fe7e97ccca8
     1.1 --- a/src/HOL/Library/Mapping.thy	Sun Apr 11 16:51:05 2010 +0200
     1.2 +++ b/src/HOL/Library/Mapping.thy	Sun Apr 11 16:51:06 2010 +0200
     1.3 @@ -122,6 +122,10 @@
     1.4    "bulkload xs = tabulate [0..<length xs] (nth xs)"
     1.5    by (rule mapping_eqI) (simp add: expand_fun_eq)
     1.6  
     1.7 +lemma is_empty_empty:
     1.8 +  "is_empty m \<longleftrightarrow> m = Mapping Map.empty"
     1.9 +  by (cases m) (simp add: is_empty_def)
    1.10 +
    1.11  
    1.12  subsection {* Some technical code lemmas *}
    1.13