From 78ac2e9ae8c6638697b1aeee7f28b6ba800b28c9 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 21 Jun 2002 21:39:30 +0000
Subject: GPL update

---
 acl2/acl2.el             | 4 ++--
 html/download.html       | 6 +++---
 isa/isa-syntax.el        | 4 ++--
 isa/isa.el               | 5 ++---
 isa/thy-mode.el          | 5 +++--
 isa/x-symbol-isabelle.el | 5 ++++-
 isar/isar-syntax.el      | 1 +
 isar/isar.el             | 1 +
 lego/lego-syntax.el      | 1 +
 lego/lego.el             | 1 +
 lego/x-symbol-lego.el    | 3 ++-
 twelf/twelf.el           | 4 ++--
 12 files changed, 24 insertions(+), 16 deletions(-)

diff --git a/acl2/acl2.el b/acl2/acl2.el
index d78084cd..5ae8a1dd 100644
--- a/acl2/acl2.el
+++ b/acl2/acl2.el
@@ -1,8 +1,8 @@
 ;; acl2.el   Basic Proof General instance for ACL2
 ;;
 ;; Copyright (C) 2000 LFCS Edinburgh. 
-;;
-;; Author: David Aspinall <da@dcs.ed.ac.uk>
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
+;; Author:    David Aspinall <da@dcs.ed.ac.uk>
 ;;
 ;; $Id$
 ;;
diff --git a/html/download.html b/html/download.html
index 45537fa4..a0a75d4e 100644
--- a/html/download.html
+++ b/html/download.html
@@ -32,9 +32,9 @@ you may need to download one of the
 <a href="oldrel.php">previous releases</a>.
 </p>
 <p>
-Please check the 
-<?php fileshow("ProofGeneral/COPYING","license conditions "); ?>
-for using Proof General.
+Proof General is distributed under the terms of
+the 
+<?php fileshow("ProofGeneral/COPYING","GNU General Public License"); ?>.
 <br>
 See <a href="#prereq">below</a> for software pre-requisites for running Proof General.
 </p>
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index 0f335647..234c6dfc 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -1,8 +1,8 @@
 ;; isa-syntax.el Syntax expressions for Isabelle
-;; Copyright (C) 1994-1998 LFCS Edinburgh. 
 ;;
+;; Copyright (C) 1994-1998 LFCS Edinburgh. 
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Author:      David Aspinall <da@dcs.ed.ac.uk>
-;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
 ;;
 ;; $Id$
 ;;
diff --git a/isa/isa.el b/isa/isa.el
index 5070f723..84c5f02d 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -1,8 +1,7 @@
 ;; isa-mode.el	 Emacs support for Isabelle proof assistant
 ;; Copyright (C) 1993-2000 LFCS Edinburgh, David Aspinall.
-;;
-;; Author:      David Aspinall <da@dcs.ed.ac.uk>
-;; Contact:     isa@proofgeneral.org
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
+;; Author:    David Aspinall <da@dcs.ed.ac.uk>
 ;;
 ;; $Id$
 ;;
diff --git a/isa/thy-mode.el b/isa/thy-mode.el
index 07e0ca54..9121e3dd 100644
--- a/isa/thy-mode.el
+++ b/isa/thy-mode.el
@@ -1,7 +1,8 @@
 ;; thy-mode.el - Mode for Isabelle theory files.
 ;;
-;; Author:      David Aspinall <da@dcs.ed.ac.uk>
-;; Maintainer:  Isabelle maintainer <isabelle@dcs.ed.ac.uk>
+;; Copyright (C) 1998 LFCS Edinburgh. 
+;; Author:    David Aspinall <da@dcs.ed.ac.uk>
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; Taken from Isamode, version: 3.6 1998/09/02 11:40:45
 ;;
diff --git a/isa/x-symbol-isabelle.el b/isa/x-symbol-isabelle.el
index f9938491..02c23f70 100644
--- a/isa/x-symbol-isabelle.el
+++ b/isa/x-symbol-isabelle.el
@@ -1,7 +1,10 @@
+;; x-symbol-isabelle.el   Token language "Isabelle Symbols" for package x-symbol
+;;
 ;;  ID:         $Id$
 ;;  Author:     David von Oheimb
 ;;  Copyright   1998 Technische Universitaet Muenchen
-;;  token language "Isabelle Symbols" for package x-symbol
+;;  License     GPL (GNU GENERAL PUBLIC LICENSE)
+;;
 ;;
 ;; NB: Part of Proof General distribution.
 ;;
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 7325f709..f88d7eb1 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -1,5 +1,6 @@
 ;; isar-syntax.el Syntax expressions for Isabelle/Isar
 ;; Copyright (C) 1994-1998 LFCS Edinburgh.
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; Author:      David Aspinall <da@dcs.ed.ac.uk>
 ;; Maintainer:  Markus Wenzel <wenzelm@in.tum.de>
diff --git a/isar/isar.el b/isar/isar.el
index 4425f69b..d4f4683d 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -1,5 +1,6 @@
 ;; isar.el Major mode for Isabelle/Isar proof assistant
 ;; Copyright (C) 1994-1998 LFCS Edinburgh.
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; Author:              David Aspinall <da@dcs.ed.ac.uk>
 ;; Author / Maintainer: Markus Wenzel <wenzelm@in.tum.de>
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index 363044de..e1ff82a4 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -1,6 +1,7 @@
 ;; lego-syntax.el Syntax of LEGO
 ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
 ;; Author: Thomas Kleymann and Dilip Sequeira
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk>
 
 ;;
diff --git a/lego/lego.el b/lego/lego.el
index ea49805f..18d5e728 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -1,6 +1,7 @@
 ;; lego.el Major mode for LEGO proof assistants
 ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
 ;; Author:      Thomas Kleymann and Dilip Sequeira
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk>
 
 ;;
diff --git a/lego/x-symbol-lego.el b/lego/x-symbol-lego.el
index 531810fa..c434ac46 100644
--- a/lego/x-symbol-lego.el
+++ b/lego/x-symbol-lego.el
@@ -1,6 +1,7 @@
-;; x-symbol-coq.el
+;; x-symbol-lego.el
 ;;
 ;; David Aspinall, adapted from file supplied by David von Obheimb
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
diff --git a/twelf/twelf.el b/twelf/twelf.el
index 5d712bb5..8f79509b 100644
--- a/twelf/twelf.el
+++ b/twelf/twelf.el
@@ -1,8 +1,8 @@
 ;; twelf.el  Proof General instance for Twelf
 ;;
 ;; Copyright (C) 2000 LFCS Edinburgh. 
-;;
-;; Author: David Aspinall <da@dcs.ed.ac.uk>
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
+;; Author:    David Aspinall <da@dcs.ed.ac.uk>
 ;;
 ;; $Id$
 ;;
-- 
cgit v1.2.3