changeset 32139 | e271a64f03ff |
parent 26811 | 067cceb36e26 |
--- a/src/HOL/HoareParallel/OG_Hoare.thy Wed Jul 22 14:21:52 2009 +0200 +++ b/src/HOL/HoareParallel/OG_Hoare.thy Wed Jul 22 18:02:10 2009 +0200 @@ -441,7 +441,7 @@ apply clarify apply(frule Parallel_length_post_PStar) apply clarify - apply(drule_tac j=xa in Parallel_Strong_Soundness) + apply(drule_tac j=xb in Parallel_Strong_Soundness) apply clarify apply simp apply force