changeset 41114 | f9ae7c2abf7e |
parent 40317 | 1eac228c52b3 |
child 41846 | b368a7aee46a |
--- a/src/HOL/Tools/Function/mutual.ML Sun Dec 12 21:40:59 2010 +0100 +++ b/src/HOL/Tools/Function/mutual.ML Sun Dec 12 21:41:01 2010 +0100 @@ -1,8 +1,7 @@ (* Title: HOL/Tools/Function/mutual.ML Author: Alexander Krauss, TU Muenchen -A package for general recursive function definitions. -Tools for mutual recursive definitions. +Mutual recursive function definitions. *) signature FUNCTION_MUTUAL =