# HG changeset patch
# User wenzelm
# Date 999276408 -7200
# Node ID 0f17da240450bd68e51411a2ad17ea994ebcaafb
# Parent  f8588786cc9ccaddcbff8f2b80c5b6f4669a0a9f
tuned headers;

diff -r f8588786cc9c -r 0f17da240450 src/HOL/Tools/basic_codegen.ML
--- a/src/HOL/Tools/basic_codegen.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/HOL/Tools/basic_codegen.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,9 +1,9 @@
 (*  Title:      Pure/HOL/basic_codegen.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   2000  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Code generator for inductive datatypes and recursive functions
+Code generator for inductive datatypes and recursive functions.
 *)
 
 signature BASIC_CODEGEN =
diff -r f8588786cc9c -r 0f17da240450 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/datatype_abs_proofs.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   1998  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Proofs and defintions independent of concrete representation
 of datatypes  (i.e. requiring only abstract properties such as
diff -r f8588786cc9c -r 0f17da240450 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,9 +1,9 @@
 (*  Title:      HOL/Tools/datatype_aux.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   1998  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Auxiliary functions for defining datatypes
+Auxiliary functions for defining datatypes.
 *)
 
 signature DATATYPE_AUX =
diff -r f8588786cc9c -r 0f17da240450 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/datatype_package.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   1998  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Datatype package for Isabelle/HOL.
 *)
diff -r f8588786cc9c -r 0f17da240450 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,9 +1,9 @@
 (*  Title:      HOL/Tools/datatype_prop.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   1998  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Characteristic properties of datatypes
+Characteristic properties of datatypes.
 *)
 
 signature DATATYPE_PROP =
diff -r f8588786cc9c -r 0f17da240450 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Tools/datatype_rep_proofs.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   1998  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Definitional introduction of datatypes
 Proof of characteristic theorems:
diff -r f8588786cc9c -r 0f17da240450 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,9 +1,9 @@
 (*  Title:      Pure/HOL/inductive_codegen.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   2000  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Code generator for inductive predicates
+Code generator for inductive predicates.
 *)
 
 signature INDUCTIVE_CODEGEN =
diff -r f8588786cc9c -r 0f17da240450 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,7 +1,6 @@
 (*  Title:      HOL/Tools/primrec_package.ML
     ID:         $Id$
-    Author:     Stefan Berghofer and Norbert Voelker
-    Copyright   1998  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
 
 Package for defining functions on datatypes by primitive recursion.
 *)
diff -r f8588786cc9c -r 0f17da240450 src/Pure/Proof/ROOT.ML
--- a/src/Pure/Proof/ROOT.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/Pure/Proof/ROOT.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,5 +1,7 @@
 (*  Title:      Pure/Proof/ROOT.ML
     ID:         $Id$
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Proof term operations.
 *)
diff -r f8588786cc9c -r 0f17da240450 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Proof/proof_rewrite_rules.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   2000  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Simplification function for partial proof terms involving
 meta level rules.
diff -r f8588786cc9c -r 0f17da240450 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Proof/proof_syntax.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   2000  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Function for parsing and printing proof terms.
 *)
diff -r f8588786cc9c -r 0f17da240450 src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Proof/proofchecker.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   2000  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Simple proof checker based only on the core inference rules
 of Isabelle/Pure.
diff -r f8588786cc9c -r 0f17da240450 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Proof/reconstruct.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   2000  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Reconstruction of partial proof terms.
 *)
diff -r f8588786cc9c -r 0f17da240450 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/Pure/axclass.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/axclass.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Axiomatic type class package.
 *)
diff -r f8588786cc9c -r 0f17da240450 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Aug 31 18:43:27 2001 +0200
+++ b/src/Pure/codegen.ML	Fri Aug 31 18:46:48 2001 +0200
@@ -1,9 +1,9 @@
 (*  Title:      Pure/codegen.ML
     ID:         $Id$
-    Author:     Stefan Berghofer
-    Copyright   2000  TU Muenchen
+    Author:     Stefan Berghofer, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Generic code generator
+Generic code generator.
 *)
 
 signature CODEGEN =