diff -r 6243b49498ea -r 7eadf5acdaf4 src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Tue May 04 11:00:16 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy	Tue May 04 11:00:17 2010 +0200
@@ -216,6 +216,9 @@
   and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
 unfolding noteq_refs_def noteq_arrs_def by auto
 
+lemma noteq_refs_irrefl: "r =!= r \<Longrightarrow> False"
+  unfolding noteq_refs_def by auto
+
 lemma present_new_ref: "ref_present r h \<Longrightarrow> r =!= fst (ref v h)"
   by (simp add: ref_present_def new_ref_def ref_def Let_def noteq_refs_def)