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