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,