# HG changeset patch
# User krauss
# Date 1292186461 -3600
# Node ID f9ae7c2abf7ea93f917c3f30320fdd92356293de
# Parent  b223fa19af3c17796ca1b1ca4ef0eef967ac9c2e
tuned headers

diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/context_tree.ML
--- 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 =
diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/fun.ML
--- 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 =
diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/function.ML
--- 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 =
diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/function_common.ML
--- 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 =
diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/function_core.ML
--- 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 =
diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/mutual.ML
--- 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 =
diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/pattern_split.ML
--- 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 =
diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/relation.ML
--- 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 =
diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/scnp_reconstruct.ML
--- 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 =
diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/scnp_solve.ML
--- 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.
 *)
 
 
diff -r b223fa19af3c -r f9ae7c2abf7e src/HOL/Tools/Function/termination.ML
--- 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