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/MicroJava/BV/Correct.thy
changeset 9549 40d64cb4f4e6
parent 9376 c32c5696ec2a
child 9757 1024a2d80ac0 
--- a/src/HOL/MicroJava/BV/Correct.thy	Mon Aug 07 10:29:54 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Mon Aug 07 14:32:56 2000 +0200
@@ -34,7 +34,7 @@
 	 in
          (\\<exists>rT maxl ins.
          method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and>
-	 (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = (Invoke mn pTs) \\<and>
+	(\\<exists>C' mn pTs k. pc = k+1 \\<and> ins!k = (Invoke C' mn pTs) \\<and>
          (mn,pTs) = sig0 \\<and> 
          (\\<exists>apTs D ST'.
          fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and>
isabelle