Fix URL for X-symbol

7 files changed, 9 insertions, 8 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
diff --git a/html/download.html b/html/download.html
index 9b8e4fd1..ee94ef94 100644
--- a/html/download.html
+++ b/html/download.html
@@ -142,7 +142,7 @@ Proof General:
 <ul>
 <li>
 For displaying logical and mathematical symbols, the excellent
-<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>
+<a href="http://x-symbol.sourceforge.net/">X-Symbol</a>
 package. 
 <br>It's very easy to install.  See <a href="#xsyminstall">here</a> 
 for installation notes.
diff --git a/html/features.html b/html/features.html
index 3fde03c4..a4aed865 100644
--- a/html/features.html
+++ b/html/features.html
@@ -118,7 +118,7 @@ proof assistant to add PBP support.")  ?>
   <dd>
   Proof General has a close integration with the
   powerful 
-  <a href="http://www.fmi.uni-passau.de/~wedler/x-symbol">X-Symbol</a>
+  <a href="http://x-symbol.sourceforge.net/">X-Symbol</a>
   package, which makes it easy to transparently use real symbols and
   Greek letters in your proofs.  
   <br> 
diff --git a/html/oldnews.html b/html/oldnews.html
index 2cc3c42b..ab284c0f 100644
--- a/html/oldnews.html
+++ b/html/oldnews.html
@@ -238,7 +238,7 @@ for Isabelle 99.
 </p>
 <p>
 Some recent changes have been made to the support for
-<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>,
+<a href="http://x-symbol.sourceforge.net/">X-Symbol</a>,
 so that it is easier to turn on and off, and support is now
 properly generic.  At the moment only Isabelle has 
 support implemented.
diff --git a/html/projects.html b/html/projects.html
index a1a6ba8a..00fc98b0 100644
--- a/html/projects.html
+++ b/html/projects.html
@@ -32,6 +32,7 @@ title.
 <li><?php pgproject("test","A Test Harness and Test Suite for Proof General") ?></li>
 <li><?php pgproject("hol","Proof General for HOL") ?></li>
 <li><?php pgproject("acs","Implementing Atomic Command Sequences") ?></li>
+<li><?php pgproject("pgkit","Proof General Kit (LFCS summer studentship)") ?></li>
 </ol>
 
 <h2>B. Projects not directly involving Proof General</h2>
diff --git a/html/screenshot.html b/html/screenshot.html
index 0567b83b..3cf0ccae 100644
--- a/html/screenshot.html
+++ b/html/screenshot.html
@@ -68,7 +68,7 @@ are for writing proof scripts in ML files.
 <br>
 Isabelle supports input and output in tokens which
 display as symbols using the 
-<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol">X-Symbol</a>
+<a href="http://x-symbol.sourceforge.net/">X-Symbol</a>
 package in conjunction with Proof General.  
 Here you can see some symbols in Isabelle's output.
 </p>