--- a/src/HOL/Hoare/SepLogHeap.thy Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Hoare/SepLogHeap.thy Wed Dec 21 12:02:57 2005 +0100
@@ -9,6 +9,8 @@
theory SepLogHeap imports Main begin
+declare not_None_eq [iff]
+
types heap = "(nat \<Rightarrow> nat option)"
text{* @{text "Some"} means allocated, @{text "None"} means
@@ -86,6 +88,7 @@
"\<And>p. \<lbrakk> List h1 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
by (induct ps) (auto simp add:map_add_def split:option.split)
+
lemma list_ortho_sum2[simp]:
"\<And>p. \<lbrakk> List h2 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
by (induct ps) (auto simp add:map_add_def split:option.split)