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 9376 c32c5696ec2a
parent 8119 60b606eddec8
child 9549 40d64cb4f4e6 
--- a/src/HOL/MicroJava/BV/Correct.thy	Mon Jul 17 13:59:10 2000 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Mon Jul 17 14:00:53 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 = MI(Invoke mn pTs) \\<and>
+	 (\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = (Invoke mn pTs) \\<and>
          (mn,pTs) = sig0 \\<and> 
          (\\<exists>apTs D ST'.
          fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and>
isabelle