# HG changeset patch # User haftmann # Date 1270997466 -7200 # Node ID 4ab91a42666a318c3b0c8f15f6de338d7064cb70 # Parent 1028cf8c0d1bcde2917ffd59ce5b76f022c9f1a1 lemma is_empty_empty diff -r 1028cf8c0d1b -r 4ab91a42666a src/HOL/Library/Mapping.thy --- 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.. m = Mapping Map.empty" + by (cases m) (simp add: is_empty_def) + subsection {* Some technical code lemmas *}