diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Nominal/Examples/Class3.thy
--- a/src/HOL/Nominal/Examples/Class3.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Nominal/Examples/Class3.thy	Thu May 26 17:51:22 2016 +0200
@@ -2,7 +2,7 @@
 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"
@@ -2246,7 +2246,7 @@
 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"
@@ -2359,7 +2359,7 @@
 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>)"
@@ -4927,7 +4927,7 @@
 done
 
 
-text {* typing relation *}
+text \<open>typing relation\<close>
 
 inductive
    typing :: "ctxtn \<Rightarrow> trm \<Rightarrow> ctxtc \<Rightarrow> bool" ("_ \<turnstile> _ \<turnstile> _" [100,100,100] 100)