src/HOL/Nominal/Examples/Class3.thy

 theory Class3
 imports Class2
 begin
 
-text {* 3rd Main Lemma *}
+text \<open>3rd Main Lemma\<close>
 
 lemma Cut_a_redu_elim:
   assumes a: "Cut <a>.M (x).N \<longrightarrow>\<^sub>a R"
   shows "(\<exists>M'. R = Cut <a>.M' (x).N \<and> M \<longrightarrow>\<^sub>a M') \<or>
          (\<exists>N'. R = Cut <a>.M (x).N' \<and> N \<longrightarrow>\<^sub>a N') \<or>

 apply(rule SNaI)
 apply(drule nrename_aredu)
 apply(blast)+
 done
 
-text {* helper-stuff to set up the induction *}
+text \<open>helper-stuff to set up the induction\<close>
 
 abbreviation
   SNa_set :: "trm set"
 where
   "SNa_set \<equiv> {M. SNa M}"

 apply(simp add: trm.inject)
 apply(rule sym)
 apply(simp add: alpha fresh_prod fresh_atm)
 done
 
-text {* 3rd lemma *}
+text \<open>3rd lemma\<close>
 
 lemma CUT_SNa_aux:
   assumes a1: "<a>:M \<in> (\<parallel><B>\<parallel>)"
   and     a2: "SNa M"
   and     a3: "(x):N \<in> (\<parallel>(B)\<parallel>)"

 apply(drule validn_fresh)
 apply(auto)
 done
 
 
-text {* typing relation *}
+text \<open>typing relation\<close>
 
 inductive
    typing :: "ctxtn \<Rightarrow> trm \<Rightarrow> ctxtc \<Rightarrow> bool" ("_ \<turnstile> _ \<turnstile> _" [100,100,100] 100)
 where
   TAx:    "\<lbrakk>validn \<Gamma>;validc \<Delta>; (x,B)\<in>set \<Gamma>; (a,B)\<in>set \<Delta>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Ax x a \<turnstile> \<Delta>"