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