equal
deleted
inserted
replaced
1 (* Title: HOL/Isar_Examples/Fibonacci.thy |
1 (* Title: HOL/Isar_Examples/Fibonacci.thy |
2 Author: Gertrud Bauer |
2 Author: Gertrud Bauer |
3 Copyright 1999 Technische Universitaet Muenchen |
3 Copyright 1999 Technische Universitaet Muenchen |
4 |
4 |
5 The Fibonacci function. Demonstrates the use of recdef. Original |
5 The Fibonacci function. Original |
6 tactic script by Lawrence C Paulson. |
6 tactic script by Lawrence C Paulson. |
7 |
7 |
8 Fibonacci numbers: proofs of laws taken from |
8 Fibonacci numbers: proofs of laws taken from |
9 |
9 |
10 R. L. Graham, D. E. Knuth, O. Patashnik. |
10 R. L. Graham, D. E. Knuth, O. Patashnik. |