GPL

25 files changed, 55 insertions, 60 deletions

diff --git a/generic/pg-metadata.el b/generic/pg-metadata.el
index e43ccd08..f8c3c67b 100644
--- a/generic/pg-metadata.el
+++ b/generic/pg-metadata.el
@@ -1,8 +1,8 @@
 ;; pg-metadata.el   Persistant storage of metadata for proof scripts
 ;;
 ;; Copyright (C) 2001-2 LFCS Edinburgh. 
-;; Author:      David Aspinall
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; Author:      David Aspinall <da@dcs.ed.ac.uk>
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index 0c8dbeef..963c6fd0 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -1,8 +1,8 @@
 ;; pg-pgip.el	 Functions for processing PGIP for Proof General
 ;;
 ;; Copyright (C) 2000-2002 LFCS Edinburgh. 
-;;
-;; Author: David Aspinall <da@dcs.ed.ac.uk>
+;; Author:   David Aspinall <da@dcs.ed.ac.uk>
+;; License:  GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 4b748b81..72bfe296 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -2,7 +2,7 @@
 ;;
 ;; Copyright (C) 2000-2002 LFCS Edinburgh. 
 ;; Author:     David Aspinall and others
-;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/pg-xhtml.el b/generic/pg-xhtml.el
index cc0a8cc6..c5f09ad9 100644
--- a/generic/pg-xhtml.el
+++ b/generic/pg-xhtml.el
@@ -1,8 +1,8 @@
 ;; pg-xhtml.el	 XHTML goal display for Proof General
 ;;
 ;; Copyright (C) 2002 LFCS Edinburgh. 
-;;
-;; Author: David Aspinall <da@dcs.ed.ac.uk>
+;; Author:     David Aspinall <da@dcs.ed.ac.uk>
+;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/pg-xml.el b/generic/pg-xml.el
index cd53da06..31ba1515 100644
--- a/generic/pg-xml.el
+++ b/generic/pg-xml.el
@@ -1,8 +1,8 @@
 ;; pg-xml.el	 XML functions for Proof General
 ;;
 ;; Copyright (C) 2000-2002 LFCS Edinburgh. 
-;;
-;; Author: David Aspinall <da@dcs.ed.ac.uk>
+;; Author:     David Aspinall <da@dcs.ed.ac.uk>
+;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-compat.el b/generic/proof-compat.el
index d3cd1247..80702b93 100644
--- a/generic/proof-compat.el
+++ b/generic/proof-compat.el
@@ -1,9 +1,8 @@
 ;; proof-comapt.el   Operating system and Emacs version compatibility
 ;;
 ;; Copyright (C) 2000-2002 LFCS Edinburgh. 
-;;
 ;; Author:      David Aspinall <da@dcs.ed.ac.uk> and others
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 0b678425..e35ef0a9 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1,7 +1,8 @@
 ;; proof-config.el  Proof General configuration for proof assistant
 ;;
 ;; Copyright (C) 1998-2002 LFCS Edinburgh. 
-;; Authors: David Aspinall
+;; Author:      David Aspinall <da@dcs.ed.ac.uk> and others
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
 ;;
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 7182d1bc..07e74774 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -1,10 +1,10 @@
 ;; proof-depends.el  Theorem-theorem and theorem-definition dependencies.
 ;;
 ;; Copyright (C) 2000-2002 University of Edinburgh. 
-;; Authors:      Fiona McNeill, David Aspinall.
-;;
+;; Authors:      David Aspinall <da@dcs.ed.ac.uk>
+;;	           Earlier version by Fiona McNeil.
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Status:      Experimental code
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
 ;;
 ;; $Id$
 ;; 
diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el
index d948f3b4..878d4669 100644
--- a/generic/proof-easy-config.el
+++ b/generic/proof-easy-config.el
@@ -1,8 +1,8 @@
 ;; proof-easy-config.el    Easy configuration for Proof General
 ;;
 ;; Copyright (C) 1999-2002  David Aspinall / LFCS.
-;; Author:     David Aspinall <da@dcs.ed.ac.uk>
-;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; Author:    David Aspinall <da@dcs.ed.ac.uk>
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index d7399429..4464e3a8 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -1,6 +1,7 @@
 ;; proof-indent.el Generic Indentation for Proof Assistants
+;;
 ;; Authors:	   Markus Wenzel
-;; Maintainer:     Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; License:        GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 3fc687ae..4d2dea67 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -1,9 +1,8 @@
 ;; proof-menu.el  Menus, keymaps, and misc commands for Proof General
 ;;
 ;; Copyright (C) 2000,2001 LFCS Edinburgh. 
-;; Authors:  David Aspinall
-;;
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; Authors:   David Aspinall
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 2ab738a6..38408e6b 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1,10 +1,9 @@
 ;; proof-script.el  Major mode for proof assistant script files.
 ;;
 ;; Copyright (C) 1994-2001 LFCS Edinburgh. 
-;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
-;;          Thomas Kleymann and Dilip Sequeira
-;;
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
+;;            Thomas Kleymann and Dilip Sequeira
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f22ff1e1..383bd69e 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1,10 +1,9 @@
 ;; proof-shell.el  Proof General shell mode.
 ;;
 ;; Copyright (C) 1994-2001 LFCS Edinburgh. 
-;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
-;;          Thomas Kleymann and Dilip Sequeira
-;;
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
+;;            Thomas Kleymann and Dilip Sequeira
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 2465aafe..e0d3645c 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -1,9 +1,9 @@
 ;; proof-site.el -- Loading stubs for Proof General.
 ;;		    Configuration for site and choice of provers.
 ;;
-;; Copyright (C) 1998-2001 LFCS Edinburgh. 
+;; Copyright (C) 1998-2002 LFCS Edinburgh. 
 ;; Author:      David Aspinall <da@dcs.ed.ac.uk>
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 0aac6bdd..aeef2382 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -1,8 +1,8 @@
 ;; proof-splash.el -- Splash welcome screen for Proof General
 ;;
 ;; Copyright (C) 1998-2001 LFCS Edinburgh. 
-;; Author: David Aspinall
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; Author:    David Aspinall
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 1cfea82a..77fd63c1 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -1,10 +1,9 @@
 ;; proof-syntax.el	Functions for dealing with syntax
-;; Copyright (C)	1997-2001 LFCS Edinburgh. 
 ;;
-;; Authors: David Aspinall, Healfdene Goguen, 
-;;	    Thomas Kleymann, Dilip Sequiera
-;;
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; Copyright (C) 1997-2001 LFCS Edinburgh. 
+;; Authors:   David Aspinall, Healfdene Goguen, 
+;;	      Thomas Kleymann, Dilip Sequiera
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-system.el b/generic/proof-system.el
index 9a00cdec..c5124ee6 100644
--- a/generic/proof-system.el
+++ b/generic/proof-system.el
@@ -1,9 +1,8 @@
 ;; proof-system.el   Proof General functions for interfacing with proof system.
 ;;
 ;; Copyright (C) 2000 LFCS Edinburgh. 
-;;
 ;; Author:      David Aspinall <da@dcs.ed.ac.uk>
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 8cbe56ad..406d42a1 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -1,8 +1,8 @@
 ;; proof-toolbar.el    Toolbar for Proof General
 ;;
 ;; Copyright (C) 1998,9  David Aspinall / LFCS.
-;; Author:     David Aspinall <da@dcs.ed.ac.uk>
-;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; Author:    David Aspinall <da@dcs.ed.ac.uk>
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 6878bd86..c8ffdcc6 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -1,9 +1,8 @@
 ;; proof-utils.el   Proof General utility functions
 ;;
 ;; Copyright (C) 1998-2002 LFCS Edinburgh. 
-;;
 ;; Author:      David Aspinall <da@dcs.ed.ac.uk> and others
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index 3c383b82..1087ced5 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -1,8 +1,8 @@
 ;; proof-x-symbol.el  Support for X-Symbol package
 ;;
-;; Copyright (C) 1998,9 LFCS Edinburgh. 
-;; Author: David Aspinall <da@dcs.ed.ac.uk>
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; Copyright (C) 1998-2002 LFCS Edinburgh
+;; Author:    David Aspinall <da@dcs.ed.ac.uk>
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; The X-Symbol package is currently available at
 ;; http://x-symbol.sourceforge.net/
diff --git a/generic/proof.el b/generic/proof.el
index 2578259c..838cde0e 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1,11 +1,9 @@
 ;; proof.el	 Proof General loader.  All files require this one.
 ;;
 ;; Copyright (C) 1998-2002 LFCS Edinburgh. 
-;;
-;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
-;;          Thomas Kleymann and Dilip Sequeira
-;;
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
+;;            Thomas Kleymann and Dilip Sequeira
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/generic/span-extent.el b/generic/span-extent.el
index 019dd1b2..4f0a7cda 100644
--- a/generic/span-extent.el
+++ b/generic/span-extent.el
@@ -1,7 +1,8 @@
 ;; This file implements spans in terms of extents, for xemacs.
+;;
 ;; Copyright (C) 1998 LFCS Edinburgh
 ;; Author:	Healfdene Goguen
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 
diff --git a/generic/span-overlay.el b/generic/span-overlay.el
index ad2374f1..e626aefa 100644
--- a/generic/span-overlay.el
+++ b/generic/span-overlay.el
@@ -1,8 +1,8 @@
 ;; This file implements spans in terms of extents, for emacs19.
+;;
 ;; Copyright (C) 1998 LFCS Edinburgh
 ;; Author:	Healfdene Goguen
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
-;;
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 
diff --git a/generic/span.el b/generic/span.el
index 5480d010..86785e93 100644
--- a/generic/span.el
+++ b/generic/span.el
@@ -1,7 +1,8 @@
 ;; span.el	Datatype of "spans" for Proof General.
+;;
 ;; Copyright (C) 1998 LFCS Edinburgh
-;; Author:	Healfdene Goguen
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
+;; Author:    Healfdene Goguen
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 
diff --git a/generic/texi-docstring-magic.el b/generic/texi-docstring-magic.el
index dc16d4ad..9258ee62 100644
--- a/generic/texi-docstring-magic.el
+++ b/generic/texi-docstring-magic.el
@@ -1,9 +1,9 @@
 ;; texi-docstring-magic.el -- munge internal docstrings into texi
 ;;
 ;; Keywords: lisp, docs, tex
-;; Author: David Aspinall <da@dcs.ed.ac.uk>
-;; Copyright (C) 1998 David Aspinall
-;; Maintainer:  David Aspinall <da@dcs.ed.ac.uk>
+;; Author:     David Aspinall <da@dcs.ed.ac.uk>
+;; Copyright   (C) 1998 David Aspinall
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;