--- a/src/HOL/HOLCF/FOCUS/FOCUS.thy Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/FOCUS/FOCUS.thy Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
Author: David von Oheimb, TU Muenchen
*)
-section {* Top level of FOCUS *}
+section \<open>Top level of FOCUS\<close>
theory FOCUS
imports Fstream