| changeset 24075 | 366d4d234814 |
| parent 23894 | 1a4167d761ac |
| child 25112 | 98824cc791c0 |
--- a/src/HOL/HoareParallel/OG_Examples.thy Mon Jul 30 19:46:15 2007 +0200 +++ b/src/HOL/HoareParallel/OG_Examples.thy Tue Jul 31 00:56:26 2007 +0200 @@ -443,7 +443,7 @@ --{* 32 subgoals left *} apply(tactic {* ALLGOALS (clarify_tac @{claset}) *}) -apply(tactic {* TRYALL simple_arith_tac *}) +apply(tactic {* TRYALL (simple_arith_tac @{context}) *}) --{* 9 subgoals left *} apply (force simp add:less_Suc_eq) apply(drule sym)