| changeset 41114 | f9ae7c2abf7e |
| parent 39276 | 2ad95934521f |
| child 41417 | 211dbd42f95d |
--- 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 =