src/HOL/Nominal/Examples/Fsub.thy

   and     b: "T closed_in \<Gamma>"
   shows "\<Gamma> \<turnstile> T <: T"
 using a b
 apply(nominal_induct T avoiding: \<Gamma> rule: ty.strong_induct)
 apply(auto simp add: ty.supp abs_supp supp_atm closed_in_def)
-  \<comment>\<open>Too bad that this instantiation cannot be found automatically by
+  \<comment> \<open>Too bad that this instantiation cannot be found automatically by
   \isakeyword{auto}; \isakeyword{blast} would find it if we had not used 
   an explicit definition for \<open>closed_in_def\<close>.\<close>
 apply(drule_tac x="(TVarB tyvrs ty2)#\<Gamma>" in meta_spec)
 apply(force dest: fresh_dom simp add: closed_in_def)
 done

       }
       ultimately show "\<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: T" by blast
     qed
   } note transitivity_lemma = this  
 
-  { \<comment>\<open>The transitivity proof is now by the auxiliary lemma.\<close>
+  { \<comment> \<open>The transitivity proof is now by the auxiliary lemma.\<close>
     case 1 
     from \<open>\<Gamma> \<turnstile> S <: Q\<close> and \<open>\<Gamma> \<turnstile> Q <: T\<close>
     show "\<Gamma> \<turnstile> S <: T" by (rule transitivity_lemma) 
   next 
     case 2