license change to BSD
authorkleing
Tue Jun 29 11:18:34 2004 +0200 (2004-06-29)
changeset 1501072fbe711e414
parent 15009 8c89f588c7aa
child 15011 35be762f58f9
license change to BSD
lib/Tools/display
lib/Tools/print
lib/texinputs/draft.tex
src/HOL/LOrder.thy
src/HOL/OrderedGroup.thy
src/HOL/Ring_and_Field.thy
src/HOL/ex/Records.thy
src/Pure/General/output.ML
src/Pure/General/xml.ML
src/Pure/Isar/constdefs.ML
src/Pure/proof_general.ML
     1.1 --- a/lib/Tools/display	Tue Jun 29 10:07:56 2004 +0200
     1.2 +++ b/lib/Tools/display	Tue Jun 29 11:18:34 2004 +0200
     1.3 @@ -2,7 +2,6 @@
     1.4  #
     1.5  # $Id$
     1.6  # Author: Markus Wenzel, TU Muenchen
     1.7 -# License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.8  #
     1.9  # DESCRIPTION: display document (in DVI format)
    1.10  
     2.1 --- a/lib/Tools/print	Tue Jun 29 10:07:56 2004 +0200
     2.2 +++ b/lib/Tools/print	Tue Jun 29 11:18:34 2004 +0200
     2.3 @@ -2,7 +2,6 @@
     2.4  #
     2.5  # $Id$
     2.6  # Author: Markus Wenzel, TU Muenchen
     2.7 -# License: GPL (GNU GENERAL PUBLIC LICENSE)
     2.8  #
     2.9  # DESCRIPTION: print document
    2.10  
     3.1 --- a/lib/texinputs/draft.tex	Tue Jun 29 10:07:56 2004 +0200
     3.2 +++ b/lib/texinputs/draft.tex	Tue Jun 29 11:18:34 2004 +0200
     3.3 @@ -1,6 +1,5 @@
     3.4  %%
     3.5  %% Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
     3.6 -%% License: GPL (GNU GENERAL PUBLIC LICENSE)
     3.7  %%
     3.8  %% root for draft documents
     3.9  %%
     4.1 --- a/src/HOL/LOrder.thy	Tue Jun 29 10:07:56 2004 +0200
     4.2 +++ b/src/HOL/LOrder.thy	Tue Jun 29 11:18:34 2004 +0200
     4.3 @@ -1,7 +1,6 @@
     4.4  (*  Title:   HOL/LOrder.thy
     4.5      ID:      $Id$
     4.6      Author:  Steven Obua, TU Muenchen
     4.7 -    License: GPL (GNU GENERAL PUBLIC LICENSE)
     4.8  *)
     4.9  
    4.10  header {* Lattice Orders *}
     5.1 --- a/src/HOL/OrderedGroup.thy	Tue Jun 29 10:07:56 2004 +0200
     5.2 +++ b/src/HOL/OrderedGroup.thy	Tue Jun 29 11:18:34 2004 +0200
     5.3 @@ -1,7 +1,6 @@
     5.4  (*  Title:   HOL/OrderedGroup.thy
     5.5      ID:      $Id$
     5.6      Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel
     5.7 -    License: GPL (GNU GENERAL PUBLIC LICENSE)
     5.8  *)
     5.9  
    5.10  header {* Ordered Groups *}
     6.1 --- a/src/HOL/Ring_and_Field.thy	Tue Jun 29 10:07:56 2004 +0200
     6.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Jun 29 11:18:34 2004 +0200
     6.3 @@ -1,7 +1,6 @@
     6.4  (*  Title:   HOL/Ring_and_Field.thy
     6.5      ID:      $Id$
     6.6      Author:  Gertrud Bauer, Steven Obua, Lawrence C Paulson and Markus Wenzel
     6.7 -    License: GPL (GNU GENERAL PUBLIC LICENSE)
     6.8  *)
     6.9  
    6.10  header {* (Ordered) Rings and Fields *}
     7.1 --- a/src/HOL/ex/Records.thy	Tue Jun 29 10:07:56 2004 +0200
     7.2 +++ b/src/HOL/ex/Records.thy	Tue Jun 29 11:18:34 2004 +0200
     7.3 @@ -2,7 +2,6 @@
     7.4      ID:         $Id$
     7.5      Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, 
     7.6                  TU Muenchen
     7.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     7.8  *)
     7.9  
    7.10  header {* Using extensible records in HOL -- points and coloured points *}
     8.1 --- a/src/Pure/General/output.ML	Tue Jun 29 10:07:56 2004 +0200
     8.2 +++ b/src/Pure/General/output.ML	Tue Jun 29 11:18:34 2004 +0200
     8.3 @@ -1,7 +1,6 @@
     8.4  (*  Title:      Pure/General/output.ML
     8.5      ID:         $Id$
     8.6      Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     8.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     8.8  
     8.9  Output channels and diagnostic messages.
    8.10  *)
     9.1 --- a/src/Pure/General/xml.ML	Tue Jun 29 10:07:56 2004 +0200
     9.2 +++ b/src/Pure/General/xml.ML	Tue Jun 29 11:18:34 2004 +0200
     9.3 @@ -1,7 +1,6 @@
     9.4  (*  Title:      Pure/General/xml.ML
     9.5      ID:         $Id$
     9.6      Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
     9.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     9.8  
     9.9  Basic support for XML.
    9.10  *)
    10.1 --- a/src/Pure/Isar/constdefs.ML	Tue Jun 29 10:07:56 2004 +0200
    10.2 +++ b/src/Pure/Isar/constdefs.ML	Tue Jun 29 11:18:34 2004 +0200
    10.3 @@ -1,7 +1,6 @@
    10.4  (*  Title:      Pure/Isar/constdefs.ML
    10.5      ID:         $Id$
    10.6      Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
    10.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    10.8  
    10.9  Standard constant definitions, with type-inference and optional
   10.10  structure context; specifications need to observe strictly sequential
    11.1 --- a/src/Pure/proof_general.ML	Tue Jun 29 10:07:56 2004 +0200
    11.2 +++ b/src/Pure/proof_general.ML	Tue Jun 29 11:18:34 2004 +0200
    11.3 @@ -1,7 +1,6 @@
    11.4  (*  Title:      Pure/proof_general.ML
    11.5      ID:         $Id$
    11.6      Author:     David Aspinall and Markus Wenzel
    11.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
    11.8  
    11.9  Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk).
   11.10  *)