diff -r fae6233c5f37 -r 8ffc4d0e652d src/HOL/HOLCF/FOCUS/Buffer_adm.thy
--- a/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/FOCUS/Buffer_adm.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     David von Oheimb, TU Muenchen
 *)
 
-section {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *}
+section \<open>One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility\<close>
 
 theory Buffer_adm
 imports Buffer Stream_adm