--- 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 =
--- 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 =
--- 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 =
--- 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 =
--- 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 =
--- 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 =
--- 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 =
--- 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 `%%;