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)