diff -r b42d7983a822 -r 1fdecd15437f src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Mon Mar 17 17:37:48 2003 +0100
+++ b/src/HOL/Hoare/Separation.thy	Mon Mar 17 18:38:50 2003 +0100
@@ -64,7 +64,7 @@
 
 lemma "VARS H x y z w
  {[x\<mapsto>y] ** [z\<mapsto>w]}
- SKIP
+ y := w
  {x \<noteq> z}"
 apply vcg
 apply(auto simp:star_def R_def singl_def)