changeset 54892 | 64c2d4f8d981 |
parent 37672 | 645eb9fec794 |
child 55640 | abc140f21caa |
--- a/src/HOL/Isar_Examples/Fibonacci.thy Wed Jan 01 11:35:21 2014 +0100 +++ b/src/HOL/Isar_Examples/Fibonacci.thy Wed Jan 01 15:55:11 2014 +0100 @@ -2,7 +2,7 @@ Author: Gertrud Bauer Copyright 1999 Technische Universitaet Muenchen -The Fibonacci function. Demonstrates the use of recdef. Original +The Fibonacci function. Original tactic script by Lawrence C Paulson. Fibonacci numbers: proofs of laws taken from