diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Imperative_HOL/Imperative_HOL.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL.thy	Thu May 26 17:51:22 2016 +0200
@@ -2,7 +2,7 @@
     Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
 *)
 
-section {* Entry point into monadic imperative HOL *}
+section \<open>Entry point into monadic imperative HOL\<close>
 
 theory Imperative_HOL
 imports Array Ref