summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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,