--- a/src/HOL/HoareParallel/OG_Tactics.thy Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/HoareParallel/OG_Tactics.thy Thu May 30 10:12:52 2002 +0200
@@ -265,8 +265,7 @@
\<and> (x#xs) ! 0=x \<and> (x#xs) ! Suc n = xs ! n"
by simp
lemma le_Suc_eq_insert: "{i. i <Suc n} = insert n {i. i< n}"
-apply auto
-by arith
+by auto
lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps"
lemmas my_simp_list = list_lemmas fst_conv snd_conv
not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc Suc_Suc_eq
@@ -498,4 +497,4 @@
(Method.SIMPLE_METHOD' HEADGOAL (disjE_Tac (K all_tac))) *}
"verification condition generator for interference freedom tests"
-end
\ No newline at end of file
+end