--- a/src/HOL/Isar_Examples/Fibonacci.thy Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy Sat Dec 26 15:44:14 2015 +0100
@@ -18,9 +18,8 @@
imports "../Number_Theory/Primes"
begin
-text_raw \<open>\footnote{Isar version by Gertrud Bauer. Original tactic
- script by Larry Paulson. A few proofs of laws taken from
- @{cite "Concrete-Math"}.}\<close>
+text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
+ Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
declare One_nat_def [simp]