# 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. *)