--- a/src/HOL/Tools/inductive_package.ML Thu Oct 18 21:22:40 2001 +0200
+++ b/src/HOL/Tools/inductive_package.ML Thu Oct 18 21:27:47 2001 +0200
@@ -3,8 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Author: Stefan Berghofer, TU Muenchen
Author: Markus Wenzel, TU Muenchen
- Copyright 1994 University of Cambridge
- 1998 TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
(Co)Inductive Definition module for HOL.
--- a/src/HOL/Tools/primrec_package.ML Thu Oct 18 21:22:40 2001 +0200
+++ b/src/HOL/Tools/primrec_package.ML Thu Oct 18 21:27:47 2001 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/Tools/primrec_package.ML
ID: $Id$
Author: Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
Package for defining functions on datatypes by primitive recursion.
*)