| changeset 16733 | 236dfafbeb63 |
| parent 16417 | 9bc16273c2d4 |
| child 27651 | 16a26996c30e |
--- a/src/HOL/HoareParallel/RG_Examples.thy Thu Jul 07 12:36:56 2005 +0200 +++ b/src/HOL/HoareParallel/RG_Examples.thy Thu Jul 07 12:39:17 2005 +0200 @@ -228,7 +228,7 @@ apply simp apply clarify apply simp -apply(force elim:Example2_lemma2_Suc0) +apply(simp add:Example2_lemma2_Suc0 cong:if_cong) apply simp+ done