changeset 41114 | f9ae7c2abf7e |
parent 39288 | f1ae2493d93f |
child 41417 | 211dbd42f95d |
--- 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 =