diff options
| -rw-r--r-- | BUGS | 2 | ||||
| -rw-r--r-- | FAQ | 2 | ||||
| -rw-r--r-- | README | 22 | ||||
| -rw-r--r-- | doc/PG-adapting.texi | 10 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 30 | ||||
| -rw-r--r-- | doc/README.doc | 2 | ||||
| -rw-r--r-- | etc/ProofGeneral.spec | 4 | ||||
| -rw-r--r-- | generic/proof-config.el | 2 | ||||
| -rw-r--r-- | generic/proof-utils.el | 2 | ||||
| -rw-r--r-- | html/about.phtml | 6 | ||||
| -rw-r--r-- | html/cvsweb.conf | 14 | ||||
| -rw-r--r-- | html/devel.phtml | 2 | ||||
| -rw-r--r-- | html/oldnews.phtml | 2 | ||||
| -rw-r--r-- | papers/README | 2 |
14 files changed, 46 insertions, 56 deletions
@@ -3,7 +3,7 @@ * Known Bugs and Workarounds for Proof General. Contact: mailto:proofgen@dcs.ed.ac.uk -See also: http://www.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS +See also: http://www.proofgeneral.org/ProofGeneral/BUGS Generic bugs are listed here, which may affect all of the supported provers. See lego/BUGS coq/BUGS, etc, for specific bug lists for each @@ -3,7 +3,7 @@ FAQs for Proof General $Id$ -For latest version, see http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneral/FAQ +For latest version, see http://www.proofgeneral.org/ProofGeneral/FAQ ----------------------------------------------------------------- @@ -19,34 +19,24 @@ See doc/ for documentation of Proof General. For notes on the supported assistants, see the README files in subdirectories: + af2/ AF2 + coq/ Coq isa/ Isabelle isar/ Isabelle/Isar - coq/ Coq lego/ LEGO hol98/ HOL 98 - plastic/ Plastic + plastic/ Plastic [ in development release only ] + twelf/ Twelf [ in development release only ] Check BUGS for problems and issues, in this directory, and for specific issues, in each prover subdirectory. For the latest news and downloads, check the Proof General web page -at: http://www.lfcs.informatics.ed.ac.uk/proofgen +at: http://www.proofgeneral.org David Aspinall. -March 2000. - ----- - -NEWSFLASH: - -For the forseeable future, all Proof General pages are hosted on my -personal server, zermelo.dcs.ed.ac.uk, so replace "www.dcs" or -"www.lfcs.informatics" by "zermelo.dcs" in all URLs mentioned in the -sources and documentation. (There is an indirection in place via -www.lfcs.informatics but it is not totally reliable, unfortunately) - - +November 2000. diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index f6cb3a40..0cf8fb28 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -15,7 +15,7 @@ @paragraphindent 0 @c A flag for whether to include the front image in the @c DVI file. You can download the front image from -@c http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneralPortrait.eps.gz +@c http://www.proofgeneral.org/ProofGeneralPortrait.eps.gz @c then put it into this directory and 'make dvi' (pdf,ps) @c will set the flag below automatically. @clear haveeps @@ -29,10 +29,10 @@ @c so removed for now. @set URLxsymbol http://www.fmi.uni-passau.de/~wedler/x-symbol/ @set URLisamode http://zermelo.dcs.ed.ac.uk/~isamode -@set URLpghome http://zermelo.dcs.ed.ac.uk/home/proofgen -@set URLpglatestrpm http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.noarch.rpm -@set URLpglatesttar http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.tar.gz -@set URLpglatestdev http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz +@set URLpghome http://www.proofgeneral.org +@set URLpglatestrpm http://www.proofgeneral.org/ProofGeneral-latest.noarch.rpm +@set URLpglatesttar http://www.proofgeneral.org/ProofGeneral-latest.tar.gz +@set URLpglatestdev http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz @c @c diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 888ab292..57a14b65 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -15,7 +15,7 @@ @paragraphindent 0 @c A flag for whether to include the front image in the @c DVI file. You can download the front image from -@c http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneralPortrait.eps.gz +@c http://www.proofgeneral.org/ProofGeneralPortrait.eps.gz @c then put it into this directory and 'make dvi' (pdf,ps) @c will set the flag below automatically. @clear haveeps @@ -28,11 +28,11 @@ @c FIXME: unfortunately, broken in buggy pdftexinfo. @c so removed for now. @set URLxsymbol http://www.fmi.uni-passau.de/~wedler/x-symbol/ -@set URLisamode http://zermelo.dcs.ed.ac.uk/~isamode -@set URLpghome http://zermelo.dcs.ed.ac.uk/home/proofgen -@set URLpglatestrpm http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.noarch.rpm -@set URLpglatesttar http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.tar.gz -@set URLpglatestdev http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz +@set URLisamode http://www.proofgeneral.org/~isamode +@set URLpghome http://www.proofgeneral.org +@set URLpglatestrpm http://www.proofgeneral.org/ProofGeneral-latest.noarch.rpm +@set URLpglatesttar http://www.proofgeneral.org/ProofGeneral-latest.tar.gz +@set URLpglatestdev http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz @c @c @@ -192,7 +192,7 @@ some history about previous releases, and acknowledgements to those who have helped along the way. Proof General has a home page at -@uref{http://www.lfcs.informatics.ed.ac.uk/proofgen}. +@uref{http://www.proofgeneral.org}. Visit this page for the latest version of this manual, other documentation, system downloads, etc. @@ -367,7 +367,7 @@ interact with the LEGO system. David Aspinall convinced Thomas Kleymann that programming in Emacs Lisp wasn't so difficult after all. In fact, Aspinall had already implemented an Emacs interface for Isabelle with bells and whistles, -called @uref{http://zermelo.dcs.ed.ac.uk/~isamode,Isamode}. Soon +called @uref{http://www.proofgeneral.org/~isamode,Isamode}. Soon after, the package @code{lego-mode} was born. Users were able to develop proof scripts in one buffer. Support was provided to automatically send parts of the script to the proof process. The last official version with @@ -3175,7 +3175,7 @@ loader for proper automatic multiple file handling. Isabelle Proof General includes a mode for editing theory files taken from David Aspinall's Isamode interface, see -@uref{http://zermelo.dcs.ed.ac.uk/~isamode}. Detailed documentation +@uref{http://www.proofgeneral.org/~isamode}. Detailed documentation for the theory file mode is included with @code{Isamode}, there are some notes on the special functions available and customization settings below. @@ -3500,7 +3500,7 @@ large or heavy committment. @appendix Obtaining and Installing Proof General has its own -@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen,home page} hosted at +@uref{http://www.proofgeneral.org,home page} hosted at Edinburgh. Visit this page for the latest news! STOP PRESS: the Proof General web pages are temporarily being hosted at @@ -3521,17 +3521,17 @@ STOP PRESS: the Proof General web pages are temporarily being hosted at You can obtain Proof General from the URL @example -@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen}. +@uref{http://www.proofgeneral.org}. @end example The distribution is available in three forms @itemize @bullet @item A source tarball, @* -@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz} +@uref{http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz} @item A Linux RPM package (for any architecture), @* -@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-latest.noarch.rpm} +@uref{http://www.proofgeneral.org/ProofGeneral-latest.noarch.rpm} @item A developer's tarball, @* -@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral-devel-latest.tar.gz} +@uref{http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz} @end itemize Both the source tarball and the RPM package include the generic elisp @@ -3688,7 +3688,7 @@ to find out how to disable support for provers you don't use. We mention some of the known problems with Proof General here. The list was written for Proof General 2.0. It is not a description of all bugs and may be out of date. @* Please consult the file -@uref{http://zermelo.dcs.ed.ac.uk/home/proofgen/ProofGeneral/BUGS,@file{BUGS}} +@uref{http://www.proofgeneral.org/ProofGeneral/BUGS,@file{BUGS}} in the distribution for more detailed and up-to-date information. @* If you discover a problem which isn't mentioned in @file{BUGS}, please diff --git a/doc/README.doc b/doc/README.doc index b96c85bf..e350baea 100644 --- a/doc/README.doc +++ b/doc/README.doc @@ -20,7 +20,7 @@ If you want a front image on the printed dvi/gs manuals, you need to have the ProofGeneral.eps file in this directory. You can download a compressed version from -http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneral/doc/ProofGeneral.eps.gz +http://www.proofgeneral.org/ProofGeneral/doc/ProofGeneral.eps.gz This file is not included with the distribution because it is rather large (1.6M). diff --git a/etc/ProofGeneral.spec b/etc/ProofGeneral.spec index 8f509160..1e955391 100644 --- a/etc/ProofGeneral.spec +++ b/etc/ProofGeneral.spec @@ -4,9 +4,9 @@ Version: 3.2pre000925 Release: 1 Group: Applications/Editors/Emacs Copyright: LFCS, University of Edinburgh -Url: http://www.lfcs.informatics.ed.ac.uk/proofgen +Url: http://www.proofgeneral.org/ Packager: David Aspinall <da@dcs.ed.ac.uk> -Source: http://www.dcs.ed.ac.uk/proofgen/ProofGeneral-3.2pre000925.tar.gz +Source: http://www.proofgeneral.org/proofgen/ProofGeneral-3.2pre000925.tar.gz BuildRoot: /tmp/ProofGeneral-root Patch: ProofGeneral.patch PreReq: /sbin/install-info diff --git a/generic/proof-config.el b/generic/proof-config.el index cc19b090..bc3b80fc 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -2195,7 +2195,7 @@ If this table is empty or needs adjusting, please make changes using :group 'proof-general-internals) (defcustom proof-general-home-page - "http://www.lfcs.informatics.ed.ac.uk/proofgen" + "http://www.proofgeneral.org" "*Web address for Proof General" :type 'string :group 'proof-general-internals) diff --git a/generic/proof-utils.el b/generic/proof-utils.el index d5468be6..30807443 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -542,7 +542,7 @@ Returns non-nil if response buffer was cleared." "[ When reporting a bug, please include a small test case for us to repeat it. Please also check that it is not already covered in the BUGS files that came with the distribution, or the latest versions at - http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneral/BUGS ]"))) + http://www.proofgeneral.org/ProofGeneral/BUGS ]"))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/html/about.phtml b/html/about.phtml index e3e244af..7641676d 100644 --- a/html/about.phtml +++ b/html/about.phtml @@ -1,9 +1,9 @@ <h2>About the Proof General project</h2> <p> The forefather of Proof General was LEGO mode, begun in 1994 at the <a -href="http://www.dcs.ed.ac.uk/lfcs">LFCS</a> by Thomas Kleymann. LEGO +href="http://www.lfcs.informatics.ed.ac.uk">LFCS</a> by Thomas Kleymann. LEGO mode was an Emacs-based front end for LEGO similar to David Aspinall's -<a href="http://zermelo.dcs.ed.ac.uk/~isamode">Isamode</a>, +<a href="http://www.proofgeneral.org/~isamode">Isamode</a>, developed at the LFCS since 1992. After 1994, implementations of proof-by-pointing and script management were added to LEGO mode, and the code was made generic. The generic basis was developed by @@ -22,7 +22,7 @@ EPSRC, <!-- </a>, --> the <a href="http://www.dcs.ed.ac.uk/lfcs/research/types_bra/index.html">EC</a>, -and the <a href="http://www.dcs.ed.ac.uk/lfcs">LFCS</a>. +and the <a href="http://www.lfcs.informatics.ed.ac.uk">LFCS</a>. </p> <p> diff --git a/html/cvsweb.conf b/html/cvsweb.conf index cf3b03b2..73de6277 100644 --- a/html/cvsweb.conf +++ b/html/cvsweb.conf @@ -79,7 +79,7 @@ $cvstreedefault = 'ProofGeneral'; ############## $stylesheet = '<link rel="stylesheet" - href="http://zermelo.dcs.ed.ac.uk/~proofgen/proofgen.css" + href="http://www.proofgeneral.org/proofgen.css" type="text/css">'; @@ -88,8 +88,8 @@ $stylesheet = '<link rel="stylesheet" $body_tag = '<body>'; # Wanna have a logo on the page ? -$logo = '<a href="http://zermelo.dcs.ed.ac.uk/~proofgen"> - <img src="http://zermelo.dcs.ed.ac.uk/~proofgen/images/ProofGeneral.jpg" alt="Proof General" align=top +$logo = '<a href="http://www.proofgeneral.org"> + <img src="http://www.proofgeneral.org/images/ProofGeneral.jpg" alt="Proof General" align=top width=65 height=76 border=0 ></a>'; @@ -98,7 +98,7 @@ $defaulttitle = "Proof General CVS Repository"; # This message is shown on the footer $footer = '<small> -<i>Contact <a href="http://zermelo.dcs.ed.ac.uk/~da/">David Aspinall</a> +<i>Contact <a href="http://www.proofgeneral.org/~da/">David Aspinall</a> for information about Proof General development. <br> This page was generated by @@ -342,9 +342,9 @@ $tabstop = 8; # $bighr="<hr noshade size=1>"; # $widehr="<hr noshade width=100%>"; -$hr = '<img border=0 src="http://zermelo.dcs.ed.ac.uk/~proofgen/images/silverrule.gif" height=4 width=100%>'; -$bighr = '<img border=0 src="http://zermelo.dcs.ed.ac.uk/~proofgen/images/silverrule.gif" height=8 width=100%>'; -$widehr = '<img border=0 src="http://zermelo.dcs.ed.ac.uk/~proofgen/images/silverrule.gif" height=4 width=100%>'; +$hr = '<img border=0 src="http://www.proofgeneral.org/images/silverrule.gif" height=4 width=100%>'; +$bighr = '<img border=0 src="http://www.proofgeneral.org/images/silverrule.gif" height=8 width=100%>'; +$widehr = '<img border=0 src="http://www.proofgeneral.org/images/silverrule.gif" height=4 width=100%>'; #EOF diff --git a/html/devel.phtml b/html/devel.phtml index 1b92fe2b..ce9f1d3c 100644 --- a/html/devel.phtml +++ b/html/devel.phtml @@ -22,7 +22,7 @@ for a summary of changes since the last stable version. </ul> <ul> <li> -Browse a mirror of the <a href="http://zermelo.dcs.ed.ac.uk/cgi-bin/cvsweb.cgi">Proof General CVS repository</a>. <br> +Browse a mirror of the <a href="http://www.proofgeneral.org/cgi-bin/cvsweb.cgi">Proof General CVS repository</a>. <br> <i>Note:</i> this mirror is updated nightly, so it may be slightly out of date.<br> </li> diff --git a/html/oldnews.phtml b/html/oldnews.phtml index cff60a68..4078fd73 100644 --- a/html/oldnews.phtml +++ b/html/oldnews.phtml @@ -21,7 +21,7 @@ Thanks to Markus Wenzel and Pierre Lescanne for reporting problems. <p> New! For developers, a web-browsable mirror of the Proof General cvs is available -<a href="http://zermelo.dcs.ed.ac.uk/cgi-bin/cvsweb.cgi">here</a>. +<a href="http://www.proofgeneral.org/cgi-bin/cvsweb.cgi">here</a>. </p> <li><b>5th May 2000</b> <p> diff --git a/papers/README b/papers/README index 121b6666..8d106538 100644 --- a/papers/README +++ b/papers/README @@ -1,4 +1,4 @@ Papers are not included with the distribution at the moment. Please look under "Documentation" on the Proof General home page, -http://zermelo.dcs.ed.ac.uk/~proofgen +http://www.proofgeneral.org |