| changeset 41114 | f9ae7c2abf7e | 
| parent 40317 | 1eac228c52b3 | 
| child 41117 | d6379876ec4c | 
--- a/src/HOL/Tools/Function/context_tree.ML Sun Dec 12 21:40:59 2010 +0100 +++ b/src/HOL/Tools/Function/context_tree.ML Sun Dec 12 21:41:01 2010 +0100 @@ -1,8 +1,7 @@ (* Title: HOL/Tools/Function/context_tree.ML Author: Alexander Krauss, TU Muenchen -A package for general recursive function definitions. -Builds and traverses trees of nested contexts along a term. +Construction and traversal of trees of nested contexts along a term. *) signature FUNCTION_CTXTREE =