author | paulson |
Fri, 04 Jul 1997 11:56:49 +0200 | |
changeset 3494 | f7ac2d1e2051 |
parent 3493 | 124103119f1c |
child 3495 | 04739732b13e |
--- a/src/HOL/ex/Fib.thy Fri Jul 04 11:56:18 1997 +0200 +++ b/src/HOL/ex/Fib.thy Fri Jul 04 11:56:49 1997 +0200 @@ -3,8 +3,7 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge -Fibonacci numbers and other simple examples of recursive definitions - (the TFL package) +The Fibonacci function. Demonstrates the use of recdef. *) Fib = WF_Rel + Divides +