src/HOL/HoareParallel/OG_Examples.thy
changeset 16298 8435be7188cb
parent 15912 47aa1a8fcdc9
child 16417 9bc16273c2d4
--- a/src/HOL/HoareParallel/OG_Examples.thy	Mon Jun 06 13:30:05 2005 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy	Mon Jun 06 13:30:21 2005 +0200
@@ -446,7 +446,6 @@
 --{* 33 subgoals left *}
 apply(tactic {* ALLGOALS Clarify_tac *})
 
-ML "set Presburger.trace"
 apply(tactic {* TRYALL simple_arith_tac *})
 --{* 10 subgoals left *}
 apply (force simp add:less_Suc_eq)