diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Puzzle.thy
--- a/src/HOL/Isar_Examples/Puzzle.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Puzzle.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -4,12 +4,14 @@
 imports Main
 begin
 
-text_raw \<open>\footnote{A question from ``Bundeswettbewerb Mathematik''.
-  Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
-  script by Tobias Nipkow.}\<close>
+text_raw \<open>\<^footnote>\<open>A question from ``Bundeswettbewerb Mathematik''. Original
+  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by Tobias
+  Nipkow.\<close>\<close>
 
-text \<open>\<^bold>\<open>Problem.\<close> Given some function \<open>f: \<nat> \<rightarrow> \<nat>\<close> such that
-  \<open>f (f n) < f (Suc n)\<close> for all \<open>n\<close>. Demonstrate that \<open>f\<close> is the identity.\<close>
+text \<open>
+  \<^bold>\<open>Problem.\<close> Given some function \<open>f: \<nat> \<rightarrow> \<nat>\<close> such that \<open>f (f n) < f (Suc n)\<close>
+  for all \<open>n\<close>. Demonstrate that \<open>f\<close> is the identity.
+\<close>
 
 theorem
   assumes f_ax: "\<And>n. f (f n) < f (Suc n)"