diff options
| author | David Aspinall | 2002-04-23 16:53:32 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-04-23 16:53:32 +0000 |
| commit | 59bdb9ac18f8f1e2a91a00cc73274acbfa8d9611 (patch) | |
| tree | b423f02e118cb0fe701c7006ae59ca779aa224d5 /doc/ProofGeneral.texi | |
| parent | 869309b7b32de87e1f28c1838b8a0a0f2654687f (diff) | |
Fix URL for X-symbol
Diffstat (limited to 'doc/ProofGeneral.texi')
| -rw-r--r-- | doc/ProofGeneral.texi | 4 |
1 files changed, 2 insertions, 2 deletions
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 |