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.
cosmetic mod.
authornipkow
Thu, 02 Dec 1999 09:09:30 +0100
changeset 8047 3a0c996cf2b2
parent 8046 91587887bcbf
child 8048 b7f7e18eb584
cosmetic mod.
src/HOL/MicroJava/BV/Correct.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/BV/Correct.thy	Wed Dec 01 22:38:35 1999 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Dec 02 09:09:30 1999 +0100
@@ -41,7 +41,7 @@
          fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and>
          length apTs = length pTs \\<and>
          (\\<exists>D' rT' maxl' ins'.
-           method (G,D) (mn,pTs) = Some(D',rT',(maxl',ins')) \\<and>
+           method (G,D) sig0 = Some(D',rT',(maxl',ins')) \\<and>
            G \\<turnstile> rT0 \\<preceq> rT') \\<and>
 	 correct_frame G hp (tl ST, LT) maxl ins f \\<and> 
 	 correct_frames G hp phi rT sig frs))))"
isabelle