src/HOL/Isar_examples/Fibonacci.thy
changeset 31758 3edd5f813f01
parent 27556 292098f2efdf
equal deleted inserted replaced
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.