diff -r 52a87574bca9 -r 6c6ccf573479 src/HOL/MicroJava/JVM/JVMInstructions.thy
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Sat Jan 02 18:48:45 2016 +0100
@@ -9,35 +9,35 @@
 
 
 datatype 
-  instr = Load nat                  -- "load from local variable"
-        | Store nat                 -- "store into local variable"
-        | LitPush val               -- "push a literal (constant)"
-        | New cname                 -- "create object"
-        | Getfield vname cname      -- "Fetch field from object"
-        | Putfield vname cname      -- "Set field in object    "
-        | Checkcast cname           -- "Check whether object is of given type"
-        | Invoke cname mname "(ty list)"  -- "inv. instance meth of an object"
-        | Return                    -- "return from method"
-        | Pop                       -- "pop top element from opstack"
-        | Dup                       -- "duplicate top element of opstack"
-        | 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"
-        | Ifcmpeq int               -- "branch if int/ref comparison succeeds"
-        | Throw                     -- "throw top of stack as exception"
+  instr = Load nat                  \<comment> "load from local variable"
+        | Store nat                 \<comment> "store into local variable"
+        | LitPush val               \<comment> "push a literal (constant)"
+        | New cname                 \<comment> "create object"
+        | Getfield vname cname      \<comment> "Fetch field from object"
+        | Putfield vname cname      \<comment> "Set field in object    "
+        | Checkcast cname           \<comment> "Check whether object is of given type"
+        | Invoke cname mname "(ty list)"  \<comment> "inv. instance meth of an object"
+        | Return                    \<comment> "return from method"
+        | Pop                       \<comment> "pop top element from opstack"
+        | Dup                       \<comment> "duplicate top element of opstack"
+        | Dup_x1                    \<comment> "duplicate top element and push 2 down"
+        | Dup_x2                    \<comment> "duplicate top element and push 3 down"
+        | Swap                      \<comment> "swap top and next to top element"
+        | IAdd                      \<comment> "integer addition"
+        | Goto int                  \<comment> "goto relative address"
+        | Ifcmpeq int               \<comment> "branch if int/ref comparison succeeds"
+        | Throw                     \<comment> "throw top of stack as exception"
 
 type_synonym
   bytecode = "instr list"
 type_synonym
   exception_entry = "p_count \<times> p_count \<times> p_count \<times> cname" 
-                  -- "start-pc, end-pc, handler-pc, exception type"
+                  \<comment> "start-pc, end-pc, handler-pc, exception type"
 type_synonym
   exception_table = "exception_entry list"
 type_synonym
   jvm_method = "nat \<times> nat \<times> bytecode \<times> exception_table"
-   -- "max stacksize, size of register set, instruction sequence, handler table"
+   \<comment> "max stacksize, size of register set, instruction sequence, handler table"
 type_synonym
   jvm_prog = "jvm_method prog"