# HG changeset patch
# User wenzelm
# Date 1003433267 -7200
# Node ID 02825c735938782fac56325c0216c99e956cfc38
# Parent  475f772ab6436a351f62f227892894be8f5bab84
GPLed;

diff -r 475f772ab643 -r 02825c735938 src/HOL/Tools/inductive_package.ML
--- 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.
 
diff -r 475f772ab643 -r 02825c735938 src/HOL/Tools/primrec_package.ML
--- 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.
 *)