diff -r 01fc1fc61384 -r b1915d3e571d src/HOL/MicroJava/JVM/JVMInstructions.thy
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Thu Oct 24 07:23:46 2002 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Thu Oct 24 12:06:43 2002 +0200
@@ -22,8 +22,8 @@
         | Return                    -- "return from method"
         | Pop                       -- "pop top element from opstack"
         | Dup                       -- "duplicate top element of opstack"
-        | Dup_x1                    -- "duplicate next to top element"
-        | Dup_x2                    -- "duplicate 3rd element"
+        | Dup_x1                    -- "duplicate top element and push 2 down"
+        | Dup_x2                    -- "duplicate top element and push 3 down"
         | Swap                      -- "swap top and next to top element"
         | IAdd                      -- "integer addition"
         | Goto int                  -- "goto relative address"
@@ -36,7 +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>"
+   -- "max stacksize, size of register set, instruction sequence, handler table"
   jvm_prog = "jvm_method prog" 
 
 end