diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-04-23 16:53:32 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-04-23 16:53:32 +0000 |
| commit | 59bdb9ac18f8f1e2a91a00cc73274acbfa8d9611 (patch) | |
| tree | b423f02e118cb0fe701c7006ae59ca779aa224d5 /doc | |
| parent | 869309b7b32de87e1f28c1838b8a0a0f2654687f (diff) | |
Fix URL for X-symbol
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/PG-adapting.texi | 4 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 5bed9953..e6aaa24f 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -29,7 +29,7 @@ @c Some URLs. @c FIXME: unfortunately, broken in buggy pdftexinfo. @c so removed for now. -@set URLxsymbol http://www.fmi.uni-passau.de/~wedler/x-symbol/ +@set URLxsymbol http://x-symbol.sourceforge.net/ @set URLisamode http://zermelo.dcs.ed.ac.uk/~isamode @set URLpghome http://www.proofgeneral.org @set URLpglatestrpm http://www.proofgeneral.org/ProofGeneral-latest.noarch.rpm @@ -2168,7 +2168,7 @@ will magically restore the commas to the default font for you. The hack is rather painful and forces immediate fontification of files on loading (no lazy, caching locking). It is unreliable -under FSF Emacs, to boot. +under GNU Emacs, to boot. @var{lego} and Coq enable it by tradition. @end defvar diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index dc455ce0..9843074a 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -390,7 +390,7 @@ code has been moved into the Coq kernel lately. We need a volunteer from the Coq community to help to do this. An important new feature in Proof General 3.0 is support for -@uref{http://www.fmi.uni-passau.de/~wedler/x-symbol/,X-Symbol}, +@uref{http://x-symbol.sourceforge.net/,X-Symbol}, which means that real logical symbols, Greek letters, etc can be displayed during proof development, instead of their ASCII approximations. This makes Proof General a more serious competitor to @@ -2259,7 +2259,7 @@ You will be able to enable X-Symbol support if you have installed the X-Symbol package and support has been provided in Proof General for a token language for your proof assistant. The X-Symbol package is available from -@uref{http://www.fmi.uni-passau.de/~wedler/x-symbol/}. +@uref{http://x-symbol.sourceforge.net/}. Notice that for proper symbol support, the proof assistant needs to have a special @i{token language}, or a special character set, to use |