equal
deleted
inserted
replaced
16 |
16 |
17 theory Fibonacci |
17 theory Fibonacci |
18 imports "../Number_Theory/Primes" |
18 imports "../Number_Theory/Primes" |
19 begin |
19 begin |
20 |
20 |
21 text_raw \<open>\footnote{Isar version by Gertrud Bauer. Original tactic |
21 text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry |
22 script by Larry Paulson. A few proofs of laws taken from |
22 Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close> |
23 @{cite "Concrete-Math"}.}\<close> |
|
24 |
23 |
25 |
24 |
26 declare One_nat_def [simp] |
25 declare One_nat_def [simp] |
27 |
26 |
28 |
27 |