equal
deleted
inserted
replaced
13 *) |
13 *) |
14 |
14 |
15 section \<open>Fib and Gcd commute\<close> |
15 section \<open>Fib and Gcd commute\<close> |
16 |
16 |
17 theory Fibonacci |
17 theory Fibonacci |
18 imports "../Number_Theory/Primes" |
18 imports "../Computational_Algebra/Primes" |
19 begin |
19 begin |
20 |
20 |
21 text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry |
21 text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry |
22 Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close> |
22 Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close> |
23 |
23 |