src/HOL/Hoare/ExamplesAbort.thy

--- a/src/HOL/Hoare/ExamplesAbort.thy	Thu Jul 07 12:36:56 2005 +0200
+++ b/src/HOL/Hoare/ExamplesAbort.thy	Thu Jul 07 12:39:17 2005 +0200
@@ -16,7 +16,6 @@
  "VARS a i j
  {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
 apply vcg_simp
-apply arith
 done
 
 lemma "VARS (a::int list) i
@@ -27,7 +26,6 @@
  DO a[i] := 7; i := i+1 OD
  {True}"
 apply vcg_simp
-apply arith
 done
 
 end