GPLed;
authorwenzelm
Thu Oct 18 21:27:47 2001 +0200 (2001-10-18 ago)
changeset 1183402825c735938
parent 11833 475f772ab643
child 11835 13d12b99b843
GPLed;
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Oct 18 21:22:40 2001 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Oct 18 21:27:47 2001 +0200
     1.3 @@ -3,8 +3,7 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Author:     Stefan Berghofer, TU Muenchen
     1.6      Author:     Markus Wenzel, TU Muenchen
     1.7 -    Copyright   1994  University of Cambridge
     1.8 -                1998  TU Muenchen
     1.9 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    1.10  
    1.11  (Co)Inductive Definition module for HOL.
    1.12  
     2.1 --- a/src/HOL/Tools/primrec_package.ML	Thu Oct 18 21:22:40 2001 +0200
     2.2 +++ b/src/HOL/Tools/primrec_package.ML	Thu Oct 18 21:27:47 2001 +0200
     2.3 @@ -1,6 +1,7 @@
     2.4  (*  Title:      HOL/Tools/primrec_package.ML
     2.5      ID:         $Id$
     2.6      Author:     Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
     2.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.8  
     2.9  Package for defining functions on datatypes by primitive recursion.
    2.10  *)