changeset 13674 | f4c64597fb02 |
parent 12911 | 704713ca07ea |
child 13676 | b1915d3e571d |
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Wed Oct 23 16:10:02 2002 +0200 +++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Wed Oct 23 16:10:42 2002 +0200 @@ -36,6 +36,7 @@ -- "start-pc, end-pc, handler-pc, exception type" exception_table = "exception_entry list" jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table" + -- "max stacksize, length of local var array, \<dots>" jvm_prog = "jvm_method prog" end