src/HOL/Hoare/ExamplesAbort.thy

--- a/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 29 21:48:01 2011 +0200
+++ b/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 29 22:36:56 2011 +0200
@@ -14,8 +14,7 @@
 lemma
  "VARS a i j
  {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
-apply vcg_simp
-done
+by vcg_simp
 
 lemma "VARS (a::int list) i
  {True}
@@ -24,7 +23,6 @@
  INV {i <= length a}
  DO a[i] := 7; i := i+1 OD
  {True}"
-apply vcg_simp
-done
+by vcg_simp
 
 end