# HG changeset patch
# User nipkow
# Date 983312747 -3600
# Node ID 63f3e98df2a46656e27bfc8e7f74a8445f0fb52b
# Parent  1b737b4c21081535e3552a82292f5a6c2ce48ed3
*** empty log message ***

diff -r 1b737b4c2108 -r 63f3e98df2a4 src/HOL/MicroJava/BV/JVM.thy
--- 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 ==