src/HOL/Number_Theory/Fib.thy
 changeset 69597 ff784d5a5bfb parent 67051 e7e54a0b9197
     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Sat Jan 05 17:00:43 2019 +0100
1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Sat Jan 05 17:24:33 2019 +0100
1.3 @@ -42,7 +42,7 @@
1.4
1.5  text \<open>
1.6    The naive approach is very inefficient since the branching recursion leads to many
1.7 -  values of @{term fib} being computed multiple times. We can avoid this by remembering''
1.8 +  values of \<^term>\<open>fib\<close> being computed multiple times. We can avoid this by remembering''
1.9    the last two values in the sequence, yielding a tail-recursive version.
1.10    This is far from optimal (it takes roughly $O(n\cdot M(n))$ time where $M(n)$ is the
1.11    time required to multiply two $n$-bit integers), but much better than the naive version,