diff -r 6c558efcc754 -r da548623916a src/HOL/Hoare/SepLogHeap.thy
--- 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)