src/HOL/Imperative_HOL/Heap.thy
changeset 36640 7eadf5acdaf4
parent 36176 3fe7e97ccca8
child 37678 0040bafffdef
--- 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)