equal
deleted
inserted
replaced
13 (Addison-Wesley, 1989) |
13 (Addison-Wesley, 1989) |
14 *) |
14 *) |
15 |
15 |
16 header {* Fib and Gcd commute *} |
16 header {* Fib and Gcd commute *} |
17 |
17 |
18 theory Fibonacci = Primes: |
18 theory Fibonacci imports Primes begin |
19 |
19 |
20 text_raw {* |
20 text_raw {* |
21 \footnote{Isar version by Gertrud Bauer. Original tactic script by |
21 \footnote{Isar version by Gertrud Bauer. Original tactic script by |
22 Larry Paulson. A few proofs of laws taken from |
22 Larry Paulson. A few proofs of laws taken from |
23 \cite{Concrete-Math}.} |
23 \cite{Concrete-Math}.} |