1.1 --- a/src/HOL/MicroJava/BV/JVM.thy	Tue Feb 27 16:13:23 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/JVM.thy	Tue Feb 27 23:25:47 2001 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5    kiljvm :: "jvm_prog => nat => nat => ty => instr list => state list => state list"
     1.6    "kiljvm G maxs maxr rT bs ==
     1.7 -  kildall (JVMType.sl G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)"
     1.8 +  kildall (JVMType.sup G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)"
     1.9  
    1.10    wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool"
    1.11    "wt_kil G C pTs rT mxs mxl ins ==