--- 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 =
--- a/src/HOL/Tools/Function/fun.ML Sun Dec 12 21:40:59 2010 +0100
+++ b/src/HOL/Tools/Function/fun.ML Sun Dec 12 21:41:01 2010 +0100
@@ -1,8 +1,8 @@
(* Title: HOL/Tools/Function/fun.ML
Author: Alexander Krauss, TU Muenchen
-Sequential mode for function definitions
-Command "fun" for fully automated function definitions
+Command "fun": Function definitions with pattern splitting/completion
+and automated termination proofs.
*)
signature FUNCTION_FUN =
--- a/src/HOL/Tools/Function/function.ML Sun Dec 12 21:40:59 2010 +0100
+++ b/src/HOL/Tools/Function/function.ML Sun Dec 12 21:41:01 2010 +0100
@@ -1,8 +1,7 @@
(* Title: HOL/Tools/Function/function.ML
Author: Alexander Krauss, TU Muenchen
-A package for general recursive function definitions.
-Isar commands.
+Main entry points to the function package.
*)
signature FUNCTION =
--- 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 =
--- 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 =
--- 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 =
--- a/src/HOL/Tools/Function/pattern_split.ML Sun Dec 12 21:40:59 2010 +0100
+++ b/src/HOL/Tools/Function/pattern_split.ML Sun Dec 12 21:41:01 2010 +0100
@@ -2,7 +2,6 @@
Author: Alexander Krauss, TU Muenchen
Fairly ad-hoc pattern splitting.
-
*)
signature FUNCTION_SPLIT =
--- a/src/HOL/Tools/Function/relation.ML Sun Dec 12 21:40:59 2010 +0100
+++ b/src/HOL/Tools/Function/relation.ML Sun Dec 12 21:41:01 2010 +0100
@@ -1,8 +1,7 @@
(* Title: HOL/Tools/Function/relation.ML
Author: Alexander Krauss, TU Muenchen
-A package for general recursive function definitions.
-Method "relation" to commence a termination proof using a user-specified relation.
+Method "relation" to start a termination proof using a user-specified relation.
*)
signature FUNCTION_RELATION =
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Dec 12 21:40:59 2010 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Dec 12 21:41:01 2010 +0100
@@ -2,7 +2,7 @@
Author: Armin Heller, TU Muenchen
Author: Alexander Krauss, TU Muenchen
-Proof reconstruction for SCNP
+Proof reconstruction for SCNP termination.
*)
signature SCNP_RECONSTRUCT =
--- a/src/HOL/Tools/Function/scnp_solve.ML Sun Dec 12 21:40:59 2010 +0100
+++ b/src/HOL/Tools/Function/scnp_solve.ML Sun Dec 12 21:41:01 2010 +0100
@@ -2,7 +2,7 @@
Author: Armin Heller, TU Muenchen
Author: Alexander Krauss, TU Muenchen
-Generate certificates for SCNP using a SAT solver
+Certificate generation for SCNP using a SAT solver.
*)
--- a/src/HOL/Tools/Function/termination.ML Sun Dec 12 21:40:59 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML Sun Dec 12 21:41:01 2010 +0100
@@ -1,10 +1,9 @@
(* Title: HOL/Tools/Function/termination.ML
Author: Alexander Krauss, TU Muenchen
-Context data for termination proofs
+Context data for termination proofs.
*)
-
signature TERMINATION =
sig