Fix URL for X-symbol

5 files changed, 5 insertions, 4 deletions

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>