# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1430234585 -3600
# Node ID 9b0825a00b1aa7d8e79d44253c1e283e14f28715
# Parent  f0fc2378a479e2d37fcf9cc0b7bc8207716fa0aa
Fixed a non-terminating proof (almost certainly caused by no change of mind)

diff -r f0fc2378a479 -r 9b0825a00b1a src/HOL/Hoare_Parallel/OG_Examples.thy
--- 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