diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ex/TrivEx.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Trivial Abstraction Example *}
+section \<open>Trivial Abstraction Example\<close>
 
 theory TrivEx
 imports Abstraction
@@ -51,9 +51,9 @@
   "is_abstraction h_abs C_ioa A_ioa"
 apply (unfold is_abstraction_def)
 apply (rule conjI)
-txt {* start states *}
+txt \<open>start states\<close>
 apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
-txt {* step case *}
+txt \<open>step case\<close>
 apply (rule allI)+
 apply (rule imp_conj_lemma)
 apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)