--- 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)")
--- 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