src/HOL/HOLCF/ex/Loop.thy

--- a/src/HOL/HOLCF/ex/Loop.thy	Wed Jan 13 23:02:28 2016 +0100
+++ b/src/HOL/HOLCF/ex/Loop.thy	Wed Jan 13 23:07:06 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Franz Regensburger
 *)
 
-section {* Theory for a loop primitive like while *}
+section \<open>Theory for a loop primitive like while\<close>
 
 theory Loop
 imports HOLCF