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/JVM.thy
changeset 26450 158b924b5153
parent 22271 51a80e238b29
child 32960 69916a850301 
--- a/src/HOL/MicroJava/BV/JVM.thy	Thu Mar 27 19:05:10 2008 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Thu Mar 27 19:22:23 2008 +0100
@@ -11,7 +11,7 @@
 
 constdefs
   kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
-             instr list \<Rightarrow> state list \<Rightarrow> state list"
+             instr list \<Rightarrow> JVMType.state list \<Rightarrow> JVMType.state list"
   "kiljvm G maxs maxr rT et bs ==
   kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"
isabelle