Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed a non-terminating proof (almost certainly caused by no change of mind)
authorpaulson <lp15@cam.ac.uk>
Tue, 28 Apr 2015 16:23:05 +0100
changeset 60149 9b0825a00b1a
parent 60148 f0fc2378a479
child 60150 bd773c47ad0b
Fixed a non-terminating proof (almost certainly caused by no change of mind)
src/HOL/Hoare_Parallel/OG_Examples.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle