changeset 60149 | 9b0825a00b1a |
parent 59189 | ad8e0a789af6 |
child 60151 | 9023d59acce6 |
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy Mon Apr 27 15:02:51 2015 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Tue Apr 28 16:23:05 2015 +0100 @@ -192,6 +192,7 @@ --\<open>6 subgoals left\<close> prefer 6 apply(erule_tac x=i in allE) +apply simp apply fastforce --\<open>5 subgoals left\<close> prefer 5