--- a/src/HOL/MicroJava/BV/JVMType.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy Tue Jan 16 09:30:00 2018 +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" \<comment> "for Kildall"
-type_synonym method_type = "state_type option list" \<comment> "for BVSpec"
+type_synonym state = "state_type option err" \<comment> \<open>for Kildall\<close>
+type_synonym method_type = "state_type option list" \<comment> \<open>for BVSpec\<close>
type_synonym class_type = "sig \<Rightarrow> method_type"
type_synonym prog_type = "cname \<Rightarrow> class_type"