diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Thu May 26 17:51:22 2016 +0200
@@ -16,7 +16,7 @@
 
 atom_decl name
 
-text {* types and terms *}
+text \<open>types and terms\<close>
 nominal_datatype ty = 
     TVar "nat"
   | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
@@ -33,7 +33,7 @@
 by (induct T rule: ty.induct)
    (auto simp add: fresh_nat)
 
-text {* Parallel and single substitution. *}
+text \<open>Parallel and single substitution.\<close>
 fun
   lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm"   
 where
@@ -94,7 +94,7 @@
   by (nominal_induct t rule: trm.strong_induct) 
      (auto simp add: fresh_list_nil)
 
-text {* Single substitution *}
+text \<open>Single substitution\<close>
 abbreviation 
   subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100)
 where 
@@ -126,7 +126,7 @@
 by (nominal_induct e avoiding: \<theta> x e' rule: trm.strong_induct)
    (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh')
 
-text {* Typing Judgements *}
+text \<open>Typing Judgements\<close>
 
 inductive
   valid :: "(name\<times>ty) list \<Rightarrow> bool"
@@ -158,7 +158,7 @@
 using a1 a2 a3
 by (induct) (auto simp add: fresh_set fresh_prod fresh_atm)
 
-text {* Typing Relation *}
+text \<open>Typing Relation\<close>
 
 inductive
   typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
@@ -244,7 +244,7 @@
 using a b type_substitutivity_aux[where \<Delta>="[]"]
 by (auto)
 
-text {* Values *}
+text \<open>Values\<close>
 inductive
   val :: "trm\<Rightarrow>bool" 
 where
@@ -258,7 +258,7 @@
   "\<not> val (Var x)"
   by (auto elim: val.cases)
 
-text {* Big-Step Evaluation *}
+text \<open>Big-Step Evaluation\<close>
 
 inductive
   big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) 
@@ -428,7 +428,7 @@
   shows "v \<Down> v"
 using a by (simp add: values_reduce_to_themselves Vs_are_values)
 
-text {* '\<theta> maps x to e' asserts that \<theta> substitutes x with e *}
+text \<open>'\<theta> maps x to e' asserts that \<theta> substitutes x with e\<close>
 abbreviation 
   mapsto :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> bool" ("_ maps _ to _" [55,55,55] 55) 
 where