--- 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 =
--- 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
--- 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 =
--- 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.
*)
--- 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 =
--- 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:
--- 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 =
--- 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.
*)
--- 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.
*)
--- 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.
--- 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.
*)
--- 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.
--- 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.
*)
--- 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.
*)
--- 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 =