1.1 --- a/Admin/page/dist-content/packages.content	Mon May 13 09:02:13 2002 +0200
     1.2 +++ b/Admin/page/dist-content/packages.content	Mon May 13 10:40:59 2002 +0200
     1.3 @@ -20,8 +20,8 @@
     1.4  href="http://www.proofgeneral.org">Proof General</a> (please <a
     1.5  href="http://www.proofgeneral.org/register">register</a>) together
     1.6  with the (optional) <a
     1.7 -href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>
     1.8 -package.  Both of these should be used with a recent version of <a
     1.9 +href="http://x-symbol.sourceforge.net">X-Symbol</a> package.  Both of
    1.10 +these should be used with a recent version of <a
    1.11  href="http://www.xemacs.org">XEmacs-21</a> (preferably with MULE).
    1.12  
    1.13  <p>

     2.1 --- a/README.html	Mon May 13 09:02:13 2002 +0200
     2.2 +++ b/README.html	Mon May 13 10:40:59 2002 +0200
     2.3 @@ -88,7 +88,7 @@
     2.4  <p>
     2.5  
     2.6  Proof General may be used together with the Emacs
     2.7 -<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">
     2.8 +<a href="http://x-symbol.sourceforge.net">
     2.9  X-Symbol package</a>, which provides a nice way to get proper
    2.10  mathematical symbols displayed on screen.
    2.11  

     3.1 --- a/doc-src/TutorialI/preface.tex	Mon May 13 09:02:13 2002 +0200
     3.2 +++ b/doc-src/TutorialI/preface.tex	Mon May 13 10:40:59 2002 +0200
     3.3 @@ -52,11 +52,11 @@
     3.4  sessions are now run from within David Aspinall's\index{Aspinall, David}
     3.5  wonderful user interface, \hfootref{http://www.proofgeneral.org/}{Proof
     3.6    General}, even together with the
     3.7 -\hfootref{http://www.fmi.uni-passau.de/~wedler/x-symbol/}{X-Symbol} package
     3.8 -for XEmacs.  This book says very little about Proof General, which has its own
     3.9 -documentation.  In order to run Isabelle, you will need a Standard ML
    3.10 -compiler.  We recommend \hfootref{http://www.polyml.org/}{Poly/ML}, which is
    3.11 -free and gives the best performance.  The other fully supported compiler is
    3.12 +\hfootref{http://x-symbol.sourceforge.net}{X-Symbol} package for XEmacs.  This
    3.13 +book says very little about Proof General, which has its own documentation.
    3.14 +In order to run Isabelle, you will need a Standard ML compiler.  We recommend
    3.15 +\hfootref{http://www.polyml.org/}{Poly/ML}, which is free and gives the best
    3.16 +performance.  The other fully supported compiler is
    3.17  \hfootref{http://cm.bell-labs.com/cm/cs/what/smlnj/index.html}{Standard ML of
    3.18    New Jersey}.
    3.19  

     4.1 --- a/doc-src/manual.bib	Mon May 13 09:02:13 2002 +0200
     4.2 +++ b/doc-src/manual.bib	Mon May 13 10:40:59 2002 +0200
     4.3 @@ -1134,7 +1134,7 @@
     4.4  @Misc{x-symbol,
     4.5    author =	 {Christoph Wedler},
     4.6    title =	 {Emacs package ``{X-Symbol}''},
     4.7 -  note =	 {\url{http://www.fmi.uni-passau.de/~wedler/x-symbol/}}
     4.8 +  note =	 {\url{http://x-symbol.sourceforge.net}}
     4.9  }
    4.10  
    4.11  @manual{isabelle-sys,