eparation logic - a beginning.

--- a/src/HOL/Hoare/ROOT.ML	Wed May 14 11:15:18 2003 +0200
+++ b/src/HOL/Hoare/ROOT.ML	Wed May 14 14:20:55 2003 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/IMP/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
-    Copyright   1998 TUM
+    Copyright   1998-2003 TUM
 *)
 
 time_use_thy "Examples";
@@ -10,3 +10,4 @@
 time_use_thy "Pointer_Examples";
 time_use_thy "Pointer_ExamplesAbort";
 time_use_thy "SchorrWaite";
+time_use_thy "Separation";

--- a/src/HOL/Hoare/Separation.thy	Wed May 14 11:15:18 2003 +0200
+++ b/src/HOL/Hoare/Separation.thy	Wed May 14 14:20:55 2003 +0200
@@ -145,16 +145,10 @@
 proofs. Here comes a simple example of a program proof that uses a law
 of separation logic instead. *}
 
-(* move to Map.thy *)
-lemma override_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
-apply(rule ext)
-apply(fastsimp simp:override_def split:option.split)
-done
-
 (* a law of separation logic *)
 lemma star_comm: "P ** Q = Q ** P"
 apply(simp add:star_def ortho_def)
-apply(blast intro:override_comm)
+apply(blast intro:map_add_comm)
 done
 
 lemma "VARS H x y z w