diff options
34 files changed, 55 insertions, 44 deletions
@@ -1,7 +1,7 @@ ## ## Makefile for Proof General. ## -## Author: David Aspinall <da@dcs.ed.ac.uk> +## Author: David Aspinall <David.Aspinall@ed.ac.uk> ## ## make - do "compile" and "scripts" targets ## make compile - make .elc's in a single session diff --git a/Makefile.devel b/Makefile.devel index 16ef074f..c41ec028 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -2,9 +2,9 @@ ## ## Makefile for Proof General development. ## -## Author: David Aspinall <da@dcs.ed.ac.uk> +## Author: David Aspinall <David.Aspinall@ed.ac.uk> ## -## Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> +## Maintainer: Proof General maintainer <da+pg-support@inf.ed.ac.uk> ## ## Developer use only, not part of distribution. ## @@ -1,5 +1,16 @@ Proof General --- Organize your proofs! [proofgeneral.inf.ed.ac.uk] ==================================================================== + + IMPORTANT NOTE: Please note that proofgeneral.org is no longer owned + by the Proof General project; please update your links to use the + new web address http://proofgeneral.inf.ed.ac.uk. + + Report bugs, feedback, suggestions directly to me. It helps if you + use an appropriate +-extension to my mail address, e.g. + + David Aspinall <da+pg-feedback@inf.ed.ac.uk> + +==================================================================== Proof General is a generic Emacs interface for proof assistants. @@ -49,8 +60,8 @@ not mentioned in any of these files to da+pg-bugs@inf.ed.ac.uk For the latest news and downloads, visit Proof General on the web at: http://proofgeneral.inf.ed.ac.uk -David Aspinall <da+pg@inf.ed.ac.uk> -March 2003. +David Aspinall <da+pg-feedback@inf.ed.ac.uk> +February 2004. ----- @@ -8,7 +8,7 @@ and Ideas" in the manual, and for low-level detail, the file "todo" in the developer release. Please send any suggestions, comments, or offers of help to -proofgen@dcs.ed.ac.uk. Thanks! +da+pg-feedback@inf.ed.ac.uk. Thanks! Plans for upcoming versions diff --git a/acl2/acl2.el b/acl2/acl2.el index a7bf823d..90ead56a 100644 --- a/acl2/acl2.el +++ b/acl2/acl2.el @@ -2,7 +2,7 @@ ;; ;; Copyright (C) 2000 LFCS Edinburgh. ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; ;; $Id$ ;; @@ -94,6 +94,6 @@ (warn "ACL2 Proof General is incomplete! Please help improve it! -Read the manual, make improvements and send them to feedback@proofgeneral.org") +da+pg-Read the manual, make improvements and send them to feedback@inf.ed.ac.uk") (provide 'acl2) diff --git a/demoisa/demoisa-easy.el b/demoisa/demoisa-easy.el index bcd1ad9d..e0c91674 100644 --- a/demoisa/demoisa-easy.el +++ b/demoisa/demoisa-easy.el @@ -2,7 +2,7 @@ ;; ;; Copyright (C) 1999 LFCS Edinburgh. ;; -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; ;; $Id$ ;; diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el index 750853df..46c2f7b5 100644 --- a/demoisa/demoisa.el +++ b/demoisa/demoisa.el @@ -2,7 +2,7 @@ ;; ;; Copyright (C) 1999 LFCS Edinburgh. ;; -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; ;; $Id$ ;; diff --git a/generic/pg-metadata.el b/generic/pg-metadata.el index 5dcfb276..1032d684 100644 --- a/generic/pg-metadata.el +++ b/generic/pg-metadata.el @@ -1,7 +1,7 @@ ;; pg-metadata.el Persistant storage of metadata for proof scripts ;; ;; Copyright (C) 2001-2 LFCS Edinburgh. -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ @@ -112,4 +112,4 @@ -
\ No newline at end of file + diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index 61a30f2c..c185a2ff 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -1,7 +1,7 @@ ;; 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 <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ diff --git a/generic/pg-xhtml.el b/generic/pg-xhtml.el index 402e7a85..cdd84f8f 100644 --- a/generic/pg-xhtml.el +++ b/generic/pg-xhtml.el @@ -1,7 +1,7 @@ ;; 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 <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ diff --git a/generic/pg-xml.el b/generic/pg-xml.el index 7f0d48e1..8a777cbd 100644 --- a/generic/pg-xml.el +++ b/generic/pg-xml.el @@ -1,7 +1,7 @@ ;; 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 <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ diff --git a/generic/proof-compat.el b/generic/proof-compat.el index dd5d541c..2b28187e 100644 --- a/generic/proof-compat.el +++ b/generic/proof-compat.el @@ -1,7 +1,7 @@ ;; proof-compat.el Operating system and Emacs version compatibility ;; ;; Copyright (C) 2000-2002 LFCS Edinburgh. -;; Author: David Aspinall <da@dcs.ed.ac.uk> and others +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ diff --git a/generic/proof-config.el b/generic/proof-config.el index 7d2c4594..18fbffaf 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1,10 +1,10 @@ ;; proof-config.el Proof General configuration for proof assistant ;; -;; Copyright (C) 1998-2002 LFCS Edinburgh. -;; Author: David Aspinall <da@dcs.ed.ac.uk> and others +;; Copyright (C) 1998-2004 LFCS Edinburgh. +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; -;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> +;; Maintainer: Proof General maintainer <da+pg-feedback@inf.ed.ac.uk> ;; ;; $Id$ ;; @@ -421,7 +421,7 @@ signals to the remote host." ;; e) all above with GNU Emacs and XEmacs. ;; But it's difficult to keep track of all that! ;; Please report any bad/failing colour -;; combinations to proofgen@dcs.ed.ac.uk +;; combinations to da+pg-feedback@inf.ed.ac.uk ;; ;; Some of these faces aren't used by default in Proof General, ;; but you can use them in font lock patterns for specific diff --git a/generic/proof-depends.el b/generic/proof-depends.el index 57500bc8..96dbedc9 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -1,7 +1,7 @@ ;; proof-depends.el Theorem-theorem and theorem-definition dependencies. ;; ;; Copyright (C) 2000-2002 University of Edinburgh. -;; Authors: David Aspinall <da@dcs.ed.ac.uk> +;; Authors: David Aspinall <David.Aspinall@ed.ac.uk> ;; Earlier version by Fiona McNeil. ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Status: Experimental code diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el index 878d4669..97855cd4 100644 --- a/generic/proof-easy-config.el +++ b/generic/proof-easy-config.el @@ -1,7 +1,7 @@ ;; proof-easy-config.el Easy configuration for Proof General ;; ;; Copyright (C) 1999-2002 David Aspinall / LFCS. -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ diff --git a/generic/proof-site.el b/generic/proof-site.el index 42966e14..74c0004c 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -2,7 +2,7 @@ ;; Configuration for site and choice of provers. ;; ;; Copyright (C) 1998-2003 LFCS Edinburgh. -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ diff --git a/generic/proof-system.el b/generic/proof-system.el index c5124ee6..a334e82a 100644 --- a/generic/proof-system.el +++ b/generic/proof-system.el @@ -1,7 +1,7 @@ ;; proof-system.el Proof General functions for interfacing with proof system. ;; ;; Copyright (C) 2000 LFCS Edinburgh. -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ @@ -17,4 +17,4 @@ ;; End of proof-system.el -(provide 'proof-system)
\ No newline at end of file +(provide 'proof-system) diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index dde05b03..a8164b08 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -1,7 +1,7 @@ ;; proof-toolbar.el Toolbar for Proof General ;; ;; Copyright (C) 1998,9 David Aspinall / LFCS. -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 82c8c927..39416c27 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -1,7 +1,7 @@ ;; proof-utils.el Proof General utility functions ;; ;; Copyright (C) 1998-2002 LFCS Edinburgh. -;; Author: David Aspinall <da@dcs.ed.ac.uk> and others +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el index c2c19a91..7f17adc2 100644 --- a/generic/proof-x-symbol.el +++ b/generic/proof-x-symbol.el @@ -1,7 +1,7 @@ ;; proof-x-symbol.el Support for X-Symbol package ;; ;; Copyright (C) 1998-2002 LFCS Edinburgh -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Id: $Id$ ;; diff --git a/generic/span-extent.el b/generic/span-extent.el index adf85813..ffc00ca2 100644 --- a/generic/span-extent.el +++ b/generic/span-extent.el @@ -2,7 +2,7 @@ ;; ;; Copyright (C) 1998 LFCS Edinburgh ;; Author: Healfdene Goguen -;; Maintainer: David Aspinall <da@dcs.ed.ac.uk> +;; Maintainer: David Aspinall <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ diff --git a/generic/span-overlay.el b/generic/span-overlay.el index 6055e03a..1b9d4646 100644 --- a/generic/span-overlay.el +++ b/generic/span-overlay.el @@ -2,7 +2,7 @@ ;; ;; Copyright (C) 1998 LFCS Edinburgh ;; Author: Healfdene Goguen -;; Maintainer: David Aspinall <da@dcs.ed.ac.uk> +;; Maintainer: David Aspinall <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; $Id$ diff --git a/generic/texi-docstring-magic.el b/generic/texi-docstring-magic.el index cec000b2..6577ac86 100644 --- a/generic/texi-docstring-magic.el +++ b/generic/texi-docstring-magic.el @@ -1,7 +1,7 @@ ;; texi-docstring-magic.el -- munge internal docstrings into texi ;; ;; Keywords: lisp, docs, tex -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; Copyright (C) 1998 David Aspinall ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; diff --git a/hol98/hol98.el b/hol98/hol98.el index d45c321c..b6cf598b 100644 --- a/hol98/hol98.el +++ b/hol98/hol98.el @@ -2,7 +2,7 @@ ;; ;; Copyright (C) 2000 LFCS Edinburgh. ;; -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; ;; $Id$ ;; @@ -152,6 +152,6 @@ (warn "Hol Proof General is incomplete! Please help improve it! -Read the manual, make improvements and send them to proofgen@dcs.ed.ac.uk") +Read the manual, make improvements and send them to da+pg-feedback@inf.ed.ac.uk") (provide 'hol98) diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el index 00a2bd4b..3ed6c53e 100644 --- a/isa/isa-syntax.el +++ b/isa/isa-syntax.el @@ -2,7 +2,7 @@ ;; ;; Copyright (C) 1994-1998 LFCS Edinburgh. ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; ;; $Id$ ;; @@ -1,7 +1,7 @@ ; isa-mode.el Emacs support for Isabelle proof assistant ;; Copyright (C) 1993-2000 LFCS Edinburgh, David Aspinall. ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; ;; $Id$ ;; diff --git a/isa/thy-mode.el b/isa/thy-mode.el index 2bd64345..a303d961 100644 --- a/isa/thy-mode.el +++ b/isa/thy-mode.el @@ -1,7 +1,7 @@ ;; thy-mode.el - Mode for Isabelle theory files. ;; ;; Copyright (C) 1998 LFCS Edinburgh. -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; ;; Taken from Isamode, version: 3.6 1998/09/02 11:40:45 diff --git a/isar/isar-mmm.el b/isar/isar-mmm.el index 5b76f2c5..ceffa85c 100644 --- a/isar/isar-mmm.el +++ b/isar/isar-mmm.el @@ -1,7 +1,7 @@ ;; isar-mmm.el Configure MMM mode for Isar (for LaTeX, SML mode) ;; ;; Copyright (C) 2003 David Aspinall -;; Authors: David Aspinall <da@dcs.ed.ac.uk> +;; Authors: David Aspinall <David.Aspinall@ed.ac.uk> ;; Licence: GPL ;; ;; $Id$ diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 32f06efd..fe50401b 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -2,7 +2,7 @@ ;; Copyright (C) 1994-1998 LFCS Edinburgh. ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; Maintainer: Gerwin Klein <kleing@in.tum.de> ;; ;; isar-syntax.el,v 7.3 2003/04/15 16:06:09 da Exp diff --git a/isar/isar.el b/isar/isar.el index 5b4c0b97..c2897a81 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -4,7 +4,7 @@ ;; ;; Maintainer: Stefan Berghofer ;; -;; Authors: David Aspinall <da@dcs.ed.ac.uk> +;; Authors: David Aspinall <David.Aspinall@ed.ac.uk> ;; Markus Wenzel <wenzelm@in.tum.de> ;; ;; diff --git a/pgkit/pgip.el b/pgkit/pgip.el index c218a97f..30c4a687 100644 --- a/pgkit/pgip.el +++ b/pgkit/pgip.el @@ -1,7 +1,7 @@ ;; pgip.el Proof General instance for PGIP protocol (for Isabelle) ;; Copyright (C) 2003 LFCS Edinburgh. ;; -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; ;; $Id$ ;; diff --git a/twelf/twelf-font.el b/twelf/twelf-font.el index 97b68527..012bfaa7 100644 --- a/twelf/twelf-font.el +++ b/twelf/twelf-font.el @@ -2,7 +2,7 @@ ;; ;; Author: Frank Pfenning ;; Taken from Twelf's emacs mode and -;; adapted for Proof General by David Aspinall <da@dcs.ed.ac.uk> +;; adapted for Proof General by David Aspinall <David.Aspinall@ed.ac.uk> ;; ;; $Id$ ;; diff --git a/twelf/twelf-old.el b/twelf/twelf-old.el index 41e570f3..ac5273ad 100644 --- a/twelf/twelf-old.el +++ b/twelf/twelf-old.el @@ -1,7 +1,7 @@ ;; twelf-old.el Port of old Twelf Emacs mode ;; ;; Author: Frank Pfenning -;; Adapted for Proof General by David Aspinall <da@dcs.ed.ac.uk> +;; Adapted for Proof General by David Aspinall <David.Aspinall@ed.ac.uk> ;; ;; $Id$ ;; diff --git a/twelf/twelf.el b/twelf/twelf.el index ad2d9ace..b1b8f1fe 100644 --- a/twelf/twelf.el +++ b/twelf/twelf.el @@ -2,7 +2,7 @@ ;; ;; Copyright (C) 2000 LFCS Edinburgh. ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; Author: David Aspinall <David.Aspinall@ed.ac.uk> ;; ;; $Id$ ;; @@ -204,4 +204,4 @@ (cdr twelf-syntax-menu)) -(provide 'twelf)
\ No newline at end of file +(provide 'twelf) |