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.
*** empty log message ***
authornipkow
Tue, 27 Feb 2001 23:25:47 +0100
changeset 11186 63f3e98df2a4
parent 11185 1b737b4c2108
child 11187 c6e49929e544
*** empty log message ***
src/HOL/MicroJava/BV/JVM.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/BV/JVM.thy	Tue Feb 27 16:13:23 2001 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Tue Feb 27 23:25:47 2001 +0100
@@ -15,7 +15,7 @@
 
   kiljvm :: "jvm_prog => nat => nat => ty => instr list => state list => state list"
   "kiljvm G maxs maxr rT bs ==
-  kildall (JVMType.sl G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)"
+  kildall (JVMType.sup G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)"
 
   wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
   "wt_kil G C pTs rT mxs mxl ins ==
isabelle