# HG changeset patch
# User kleing
# Date 1035454003 -7200
# Node ID b1915d3e571d4ce81785a4c90f664b08f23aad88
# Parent  01fc1fc6138401a8ee2051319a3188aaf693405a
fixed latex error

diff -r 01fc1fc61384 -r b1915d3e571d src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Oct 24 07:23:46 2002 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Oct 24 12:06:43 2002 +0200
@@ -1326,12 +1326,12 @@
     apply (rule HOL.refl) apply assumption
     apply (simp add: max_ssize_def max_of_list_elem ssize_sto_def)
 
-  -- "<=s"
+  -- {* @{text "<=s"} *}
   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
   apply (frule comp_method, assumption+)
   apply (simp add: max_spec_preserves_length [THEN sym])
 
-  -- "check_type"
+  -- "@{text check_type}"
 apply (simp add: max_ssize_def ssize_sto_def max_def)
 apply (simp add: max_of_list_def)
 apply (subgoal_tac "(max (length pTsa + length ST) (length ST)) = (length pTsa + length ST)")
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