# HG changeset patch
# User haftmann
# Date 1159964266 -7200
# Node ID 9f60d493c8fe480f9b304f5e88c49e32f99f75ef
# Parent  f9cf9e62d11cb150552e0eec04409b3ffa2e3e05
clarified header comments

diff -r f9cf9e62d11c -r 9f60d493c8fe src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed Oct 04 14:17:38 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Oct 04 14:17:46 2006 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Stefan Berghofer & Florian Haftmann, TU Muenchen
 
-Code generator for inductive datatypes and type copies ("code types").
+Code generator for inductive datatypes.
 *)
 
 signature DATATYPE_CODEGEN =
diff -r f9cf9e62d11c -r 9f60d493c8fe src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Wed Oct 04 14:17:38 2006 +0200
+++ b/src/HOL/Tools/typecopy_package.ML	Wed Oct 04 14:17:46 2006 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Introducing copies of types using trivial typedefs.
+Introducing copies of types using trivial typedefs; datatype-like abstraction.
 *)
 
 signature TYPECOPY_PACKAGE =
diff -r f9cf9e62d11c -r 9f60d493c8fe src/Pure/Tools/codegen_consts.ML
--- a/src/Pure/Tools/codegen_consts.ML	Wed Oct 04 14:17:38 2006 +0200
+++ b/src/Pure/Tools/codegen_consts.ML	Wed Oct 04 14:17:46 2006 +0200
@@ -2,8 +2,9 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Distinction of ad-hoc overloaded constants. Convenient data structures
-for constants.
+Identifying constants by name plus normalized type instantantiation schemes.
+Type normalization is compatible with overloading discipline and user-defined
+ad-hoc overloading. Convenient data structures for constants.
 *)
 
 signature CODEGEN_CONSTS =
diff -r f9cf9e62d11c -r 9f60d493c8fe src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Wed Oct 04 14:17:38 2006 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Wed Oct 04 14:17:46 2006 +0200
@@ -2,7 +2,8 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Basic code generator data structures; abstract executable content of theory.
+Abstract executable content of theory. Management of data dependent on
+executabl content.
 *)
 
 signature CODEGEN_DATA =
diff -r f9cf9e62d11c -r 9f60d493c8fe src/Pure/Tools/codegen_funcgr.ML
--- a/src/Pure/Tools/codegen_funcgr.ML	Wed Oct 04 14:17:38 2006 +0200
+++ b/src/Pure/Tools/codegen_funcgr.ML	Wed Oct 04 14:17:46 2006 +0200
@@ -2,7 +2,8 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Retrieving and structuring code function theorems.
+Retrieving, normalizing and structuring code function theorems
+in graph with explicit dependencies.
 *)
 
 signature CODEGEN_FUNCGR =
diff -r f9cf9e62d11c -r 9f60d493c8fe src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Wed Oct 04 14:17:38 2006 +0200
+++ b/src/Pure/Tools/codegen_names.ML	Wed Oct 04 14:17:46 2006 +0200
@@ -3,7 +3,8 @@
     Author:     Florian Haftmann, TU Muenchen
 
 Name policies for code generation: prefixing any name by corresponding theory name,
-conversion to alphanumeric representation. Mappings are incrementally cached.
+conversion to alphanumeric representation, shallow name spaces.
+Mappings are incrementally cached.
 *)
 
 signature CODEGEN_NAMES =
diff -r f9cf9e62d11c -r 9f60d493c8fe src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Oct 04 14:17:38 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Wed Oct 04 14:17:46 2006 +0200
@@ -2,8 +2,7 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Code generator from Isabelle theories to
-intermediate language ("Thin-gol").
+Code generator extraction kernel. Code generator Isar setup.
 *)
 
 signature CODEGEN_PACKAGE =
diff -r f9cf9e62d11c -r 9f60d493c8fe src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Wed Oct 04 14:17:38 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Oct 04 14:17:46 2006 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Intermediate language ("Thin-gol") for code extraction.
+Intermediate language ("Thin-gol") representing extracted code.
 *)
 
 infix 8 `%%;