--- a/lib/Tools/display Tue Jun 29 10:07:56 2004 +0200
+++ b/lib/Tools/display Tue Jun 29 11:18:34 2004 +0200
@@ -2,7 +2,6 @@
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
-# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# DESCRIPTION: display document (in DVI format)
--- a/lib/Tools/print Tue Jun 29 10:07:56 2004 +0200
+++ b/lib/Tools/print Tue Jun 29 11:18:34 2004 +0200
@@ -2,7 +2,6 @@
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
-# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# DESCRIPTION: print document
--- a/lib/texinputs/draft.tex Tue Jun 29 10:07:56 2004 +0200
+++ b/lib/texinputs/draft.tex Tue Jun 29 11:18:34 2004 +0200
@@ -1,6 +1,5 @@
%%
%% Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
-%% License: GPL (GNU GENERAL PUBLIC LICENSE)
%%
%% root for draft documents
%%
--- a/src/HOL/LOrder.thy Tue Jun 29 10:07:56 2004 +0200
+++ b/src/HOL/LOrder.thy Tue Jun 29 11:18:34 2004 +0200
@@ -1,7 +1,6 @@
(* Title: HOL/LOrder.thy
ID: $Id$
Author: Steven Obua, TU Muenchen
- License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Lattice Orders *}
--- a/src/HOL/OrderedGroup.thy Tue Jun 29 10:07:56 2004 +0200
+++ b/src/HOL/OrderedGroup.thy Tue Jun 29 11:18:34 2004 +0200
@@ -1,7 +1,6 @@
(* Title: HOL/OrderedGroup.thy
ID: $Id$
Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel
- License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Ordered Groups *}
--- a/src/HOL/Ring_and_Field.thy Tue Jun 29 10:07:56 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy Tue Jun 29 11:18:34 2004 +0200
@@ -1,7 +1,6 @@
(* Title: HOL/Ring_and_Field.thy
ID: $Id$
Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson and Markus Wenzel
- License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* (Ordered) Rings and Fields *}
--- a/src/HOL/ex/Records.thy Tue Jun 29 10:07:56 2004 +0200
+++ b/src/HOL/ex/Records.thy Tue Jun 29 11:18:34 2004 +0200
@@ -2,7 +2,6 @@
ID: $Id$
Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel,
TU Muenchen
- License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Using extensible records in HOL -- points and coloured points *}
--- a/src/Pure/General/output.ML Tue Jun 29 10:07:56 2004 +0200
+++ b/src/Pure/General/output.ML Tue Jun 29 11:18:34 2004 +0200
@@ -1,7 +1,6 @@
(* Title: Pure/General/output.ML
ID: $Id$
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
- License: GPL (GNU GENERAL PUBLIC LICENSE)
Output channels and diagnostic messages.
*)
--- a/src/Pure/General/xml.ML Tue Jun 29 10:07:56 2004 +0200
+++ b/src/Pure/General/xml.ML Tue Jun 29 11:18:34 2004 +0200
@@ -1,7 +1,6 @@
(* Title: Pure/General/xml.ML
ID: $Id$
Author: David Aspinall, Stefan Berghofer and Markus Wenzel
- License: GPL (GNU GENERAL PUBLIC LICENSE)
Basic support for XML.
*)
--- a/src/Pure/Isar/constdefs.ML Tue Jun 29 10:07:56 2004 +0200
+++ b/src/Pure/Isar/constdefs.ML Tue Jun 29 11:18:34 2004 +0200
@@ -1,7 +1,6 @@
(* Title: Pure/Isar/constdefs.ML
ID: $Id$
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
- License: GPL (GNU GENERAL PUBLIC LICENSE)
Standard constant definitions, with type-inference and optional
structure context; specifications need to observe strictly sequential
--- a/src/Pure/proof_general.ML Tue Jun 29 10:07:56 2004 +0200
+++ b/src/Pure/proof_general.ML Tue Jun 29 11:18:34 2004 +0200
@@ -1,7 +1,6 @@
(* Title: Pure/proof_general.ML
ID: $Id$
Author: David Aspinall and Markus Wenzel
- License: GPL (GNU GENERAL PUBLIC LICENSE)
Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk).
*)