tuned headers;
authorwenzelm
Fri Aug 31 18:46:48 2001 +0200 (2001-08-31)
changeset 115390f17da240450
parent 11538 f8588786cc9c
child 11540 23794728cdb7
tuned headers;
src/HOL/Tools/basic_codegen.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/primrec_package.ML
src/Pure/Proof/ROOT.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/proofchecker.ML
src/Pure/Proof/reconstruct.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Tools/basic_codegen.ML	Fri Aug 31 18:43:27 2001 +0200
     1.2 +++ b/src/HOL/Tools/basic_codegen.ML	Fri Aug 31 18:46:48 2001 +0200
     1.3 @@ -1,9 +1,9 @@
     1.4  (*  Title:      Pure/HOL/basic_codegen.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Stefan Berghofer
     1.7 -    Copyright   2000  TU Muenchen
     1.8 +    Author:     Stefan Berghofer, TU Muenchen
     1.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.10  
    1.11 -Code generator for inductive datatypes and recursive functions
    1.12 +Code generator for inductive datatypes and recursive functions.
    1.13  *)
    1.14  
    1.15  signature BASIC_CODEGEN =
     2.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Aug 31 18:43:27 2001 +0200
     2.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Aug 31 18:46:48 2001 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      HOL/Tools/datatype_abs_proofs.ML
     2.5      ID:         $Id$
     2.6 -    Author:     Stefan Berghofer
     2.7 -    Copyright   1998  TU Muenchen
     2.8 +    Author:     Stefan Berghofer, TU Muenchen
     2.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    2.10  
    2.11  Proofs and defintions independent of concrete representation
    2.12  of datatypes  (i.e. requiring only abstract properties such as
     3.1 --- a/src/HOL/Tools/datatype_aux.ML	Fri Aug 31 18:43:27 2001 +0200
     3.2 +++ b/src/HOL/Tools/datatype_aux.ML	Fri Aug 31 18:46:48 2001 +0200
     3.3 @@ -1,9 +1,9 @@
     3.4  (*  Title:      HOL/Tools/datatype_aux.ML
     3.5      ID:         $Id$
     3.6 -    Author:     Stefan Berghofer
     3.7 -    Copyright   1998  TU Muenchen
     3.8 +    Author:     Stefan Berghofer, TU Muenchen
     3.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    3.10  
    3.11 -Auxiliary functions for defining datatypes
    3.12 +Auxiliary functions for defining datatypes.
    3.13  *)
    3.14  
    3.15  signature DATATYPE_AUX =
     4.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Aug 31 18:43:27 2001 +0200
     4.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Aug 31 18:46:48 2001 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  (*  Title:      HOL/Tools/datatype_package.ML
     4.5      ID:         $Id$
     4.6 -    Author:     Stefan Berghofer
     4.7 -    Copyright   1998  TU Muenchen
     4.8 +    Author:     Stefan Berghofer, TU Muenchen
     4.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    4.10  
    4.11  Datatype package for Isabelle/HOL.
    4.12  *)
     5.1 --- a/src/HOL/Tools/datatype_prop.ML	Fri Aug 31 18:43:27 2001 +0200
     5.2 +++ b/src/HOL/Tools/datatype_prop.ML	Fri Aug 31 18:46:48 2001 +0200
     5.3 @@ -1,9 +1,9 @@
     5.4  (*  Title:      HOL/Tools/datatype_prop.ML
     5.5      ID:         $Id$
     5.6 -    Author:     Stefan Berghofer
     5.7 -    Copyright   1998  TU Muenchen
     5.8 +    Author:     Stefan Berghofer, TU Muenchen
     5.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    5.10  
    5.11 -Characteristic properties of datatypes
    5.12 +Characteristic properties of datatypes.
    5.13  *)
    5.14  
    5.15  signature DATATYPE_PROP =
     6.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Aug 31 18:43:27 2001 +0200
     6.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Aug 31 18:46:48 2001 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4  (*  Title:      HOL/Tools/datatype_rep_proofs.ML
     6.5      ID:         $Id$
     6.6 -    Author:     Stefan Berghofer
     6.7 -    Copyright   1998  TU Muenchen
     6.8 +    Author:     Stefan Berghofer, TU Muenchen
     6.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    6.10  
    6.11  Definitional introduction of datatypes
    6.12  Proof of characteristic theorems:
     7.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Aug 31 18:43:27 2001 +0200
     7.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Aug 31 18:46:48 2001 +0200
     7.3 @@ -1,9 +1,9 @@
     7.4  (*  Title:      Pure/HOL/inductive_codegen.ML
     7.5      ID:         $Id$
     7.6 -    Author:     Stefan Berghofer
     7.7 -    Copyright   2000  TU Muenchen
     7.8 +    Author:     Stefan Berghofer, TU Muenchen
     7.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    7.10  
    7.11 -Code generator for inductive predicates
    7.12 +Code generator for inductive predicates.
    7.13  *)
    7.14  
    7.15  signature INDUCTIVE_CODEGEN =
     8.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Aug 31 18:43:27 2001 +0200
     8.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Aug 31 18:46:48 2001 +0200
     8.3 @@ -1,7 +1,6 @@
     8.4  (*  Title:      HOL/Tools/primrec_package.ML
     8.5      ID:         $Id$
     8.6 -    Author:     Stefan Berghofer and Norbert Voelker
     8.7 -    Copyright   1998  TU Muenchen
     8.8 +    Author:     Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
     8.9  
    8.10  Package for defining functions on datatypes by primitive recursion.
    8.11  *)
     9.1 --- a/src/Pure/Proof/ROOT.ML	Fri Aug 31 18:43:27 2001 +0200
     9.2 +++ b/src/Pure/Proof/ROOT.ML	Fri Aug 31 18:46:48 2001 +0200
     9.3 @@ -1,5 +1,7 @@
     9.4  (*  Title:      Pure/Proof/ROOT.ML
     9.5      ID:         $Id$
     9.6 +    Author:     Stefan Berghofer, TU Muenchen
     9.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     9.8  
     9.9  Proof term operations.
    9.10  *)
    10.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Aug 31 18:43:27 2001 +0200
    10.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Aug 31 18:46:48 2001 +0200
    10.3 @@ -1,7 +1,7 @@
    10.4  (*  Title:      Pure/Proof/proof_rewrite_rules.ML
    10.5      ID:         $Id$
    10.6 -    Author:     Stefan Berghofer
    10.7 -    Copyright   2000  TU Muenchen
    10.8 +    Author:     Stefan Berghofer, TU Muenchen
    10.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   10.10  
   10.11  Simplification function for partial proof terms involving
   10.12  meta level rules.
    11.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Aug 31 18:43:27 2001 +0200
    11.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Aug 31 18:46:48 2001 +0200
    11.3 @@ -1,7 +1,7 @@
    11.4  (*  Title:      Pure/Proof/proof_syntax.ML
    11.5      ID:         $Id$
    11.6 -    Author:     Stefan Berghofer
    11.7 -    Copyright   2000  TU Muenchen
    11.8 +    Author:     Stefan Berghofer, TU Muenchen
    11.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   11.10  
   11.11  Function for parsing and printing proof terms.
   11.12  *)
    12.1 --- a/src/Pure/Proof/proofchecker.ML	Fri Aug 31 18:43:27 2001 +0200
    12.2 +++ b/src/Pure/Proof/proofchecker.ML	Fri Aug 31 18:46:48 2001 +0200
    12.3 @@ -1,7 +1,7 @@
    12.4  (*  Title:      Pure/Proof/proofchecker.ML
    12.5      ID:         $Id$
    12.6 -    Author:     Stefan Berghofer
    12.7 -    Copyright   2000  TU Muenchen
    12.8 +    Author:     Stefan Berghofer, TU Muenchen
    12.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   12.10  
   12.11  Simple proof checker based only on the core inference rules
   12.12  of Isabelle/Pure.
    13.1 --- a/src/Pure/Proof/reconstruct.ML	Fri Aug 31 18:43:27 2001 +0200
    13.2 +++ b/src/Pure/Proof/reconstruct.ML	Fri Aug 31 18:46:48 2001 +0200
    13.3 @@ -1,7 +1,7 @@
    13.4  (*  Title:      Pure/Proof/reconstruct.ML
    13.5      ID:         $Id$
    13.6 -    Author:     Stefan Berghofer
    13.7 -    Copyright   2000  TU Muenchen
    13.8 +    Author:     Stefan Berghofer, TU Muenchen
    13.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   13.10  
   13.11  Reconstruction of partial proof terms.
   13.12  *)
    14.1 --- a/src/Pure/axclass.ML	Fri Aug 31 18:43:27 2001 +0200
    14.2 +++ b/src/Pure/axclass.ML	Fri Aug 31 18:46:48 2001 +0200
    14.3 @@ -1,6 +1,7 @@
    14.4  (*  Title:      Pure/axclass.ML
    14.5      ID:         $Id$
    14.6      Author:     Markus Wenzel, TU Muenchen
    14.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    14.8  
    14.9  Axiomatic type class package.
   14.10  *)
    15.1 --- a/src/Pure/codegen.ML	Fri Aug 31 18:43:27 2001 +0200
    15.2 +++ b/src/Pure/codegen.ML	Fri Aug 31 18:46:48 2001 +0200
    15.3 @@ -1,9 +1,9 @@
    15.4  (*  Title:      Pure/codegen.ML
    15.5      ID:         $Id$
    15.6 -    Author:     Stefan Berghofer
    15.7 -    Copyright   2000  TU Muenchen
    15.8 +    Author:     Stefan Berghofer, TU Muenchen
    15.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
   15.10  
   15.11 -Generic code generator
   15.12 +Generic code generator.
   15.13  *)
   15.14  
   15.15  signature CODEGEN =