Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Imperative_HOL/Legacy_Mrec.thy
changeset 53374 a14d2a854c02
parent 53109 186535065f5c 
--- a/src/HOL/Imperative_HOL/Legacy_Mrec.thy	Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Imperative_HOL/Legacy_Mrec.thy	Tue Sep 03 01:12:40 2013 +0200
@@ -118,7 +118,7 @@
         proof (cases "mrec b h1")
           case (Some result)
           then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastforce
-          moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
+          moreover from mrec_rec have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
             apply (intro 1(2))
             apply (auto simp add: Inr Inl')
             done
isabelle