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