src/HOL/MicroJava/Comp/CorrCompTp.thy

   apply (simp add: bc_mt_corresp_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: replST_def del: appInvoke)
   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)
     apply assumption
    apply (simp add: max_ssize_def max_of_list_elem ssize_sto_def)

   \<comment> \<open>\<open><=s\<close>\<close>
   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
   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)")
    apply simp
    apply (simp add: check_type_simps)