--- a/src/HOL/MicroJava/BV/JVMType.thy Sat Jan 02 18:46:36 2016 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Sat Jan 02 18:48:45 2016 +0100
@@ -12,8 +12,8 @@
type_synonym locvars_type = "ty err list"
type_synonym opstack_type = "ty list"
type_synonym state_type = "opstack_type \<times> locvars_type"
-type_synonym state = "state_type option err" -- "for Kildall"
-type_synonym method_type = "state_type option list" -- "for BVSpec"
+type_synonym state = "state_type option err" \<comment> "for Kildall"
+type_synonym method_type = "state_type option list" \<comment> "for BVSpec"
type_synonym class_type = "sig \<Rightarrow> method_type"
type_synonym prog_type = "cname \<Rightarrow> class_type"