diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/function_common.ML --- a/src/HOL/Tools/Function/function_common.ML Sun Dec 12 21:40:59 2010 +0100 +++ b/src/HOL/Tools/Function/function_common.ML Sun Dec 12 21:41:01 2010 +0100 @@ -1,8 +1,7 @@ (* Title: HOL/Tools/Function/function_common.ML Author: Alexander Krauss, TU Muenchen -A package for general recursive function definitions. -Common definitions and other infrastructure. +Common definitions and other infrastructure for the function package. *) signature FUNCTION_DATA =