changeset 31758 | 3edd5f813f01 |
parent 27556 | 292098f2efdf |
31757:c1262feb61c7 | 31758:3edd5f813f01 |
---|---|
1 (* Title: HOL/Isar_examples/Fibonacci.thy |
1 (* Title: HOL/Isar_examples/Fibonacci.thy |
2 ID: $Id$ |
|
3 Author: Gertrud Bauer |
2 Author: Gertrud Bauer |
4 Copyright 1999 Technische Universitaet Muenchen |
3 Copyright 1999 Technische Universitaet Muenchen |
5 |
4 |
6 The Fibonacci function. Demonstrates the use of recdef. Original |
5 The Fibonacci function. Demonstrates the use of recdef. Original |
7 tactic script by Lawrence C Paulson. |
6 tactic script by Lawrence C Paulson. |