--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Jan 16 09:30:00 2018 +0100
@@ -1269,7 +1269,7 @@
apply (intro strip)
apply (rule conjI)
- \<comment> "app"
+ \<comment> \<open>app\<close>
apply (rule Call_app [THEN app_mono_mxs])
apply assumption+
apply (rule HOL.refl)
@@ -1281,7 +1281,7 @@
apply (simp add: wf_prog_ws_prog [THEN comp_method])
apply (simp add: max_spec_preserves_length [symmetric])
- \<comment> "\<open>check_type\<close>"
+ \<comment> \<open>\<open>check_type\<close>\<close>
apply (simp add: max_ssize_def ssize_sto_def)
apply (simp add: max_of_list_def)
apply (subgoal_tac "(max (length pTsa + length ST) (length ST)) = (length pTsa + length ST)")