diff -r 124103119f1c -r f7ac2d1e2051 src/HOL/ex/Fib.thy --- 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 +