src/HOL/Hoare/Separation.thy

--- a/src/HOL/Hoare/Separation.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Hoare/Separation.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -159,9 +159,7 @@
 
 (* a law of separation logic *)
 lemma star_comm: "P ** Q = Q ** P"
-apply(simp add:star_def ortho_def)
-apply(blast intro:map_add_comm)
-done
+  by(auto simp add:star_def ortho_def dest: map_add_comm)
 
 lemma "VARS H x y z w
  {P ** Q}