src/HOL/MicroJava/JVM/JVMInstructions.thy
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