--- a/src/HOL/HoareParallel/OG_Examples.thy Tue May 18 11:45:50 2004 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Wed May 19 11:21:19 2004 +0200
@@ -445,7 +445,9 @@
apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
--{* 33 subgoals left *}
apply(tactic {* ALLGOALS Clarify_tac *})
-apply(tactic {* TRYALL arith_tac *})
+
+ML "set Presburger.trace"
+apply(tactic {* TRYALL simple_arith_tac *})
--{* 10 subgoals left *}
apply (force simp add:less_Suc_eq)
apply(drule sym)