tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.
authorchaieb
Wed, 19 May 2004 11:21:19 +0200
changeset 14757 556ce89b7d41
parent 14756 9c8cc63714f4
child 14758 af3b71a46a1c
tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.
src/HOL/HoareParallel/OG_Examples.thy
--- 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)