Fix/Update links.

Author: erikmd

about.md

@@ -7,7 +7,7 @@ subtitle:
 ## About the Proof General project
 
 The forefather of Proof General was LEGO mode, begun in 1994 at the
-[LFCS](http://www.lfcs.informatics.ed.ac.uk) by Thomas Kleymann. LEGO
+[LFCS](http://wcms.inf.ed.ac.uk/lfcs/) by Thomas Kleymann. LEGO
 mode was an Emacs-based front end for LEGO similar to David Aspinall's
 [Isamode](http://homepages.inf.ed.ac.uk/da/Isamode), developed at the
 LFCS since 1992. After 1994, implementations of proof-by-pointing and
@@ -21,7 +21,7 @@ The Proof General project was coordinated until October 1998 by Thomas
 Kleymann, and since then by David Aspinall. The project has benefited
 from travel and auxiliary support funding by
 [EPSRC](http://gow.epsrc.ac.uk/ViewGrant.aspx?GrantRef=EP/E005713/1),
-the [EC](http://www.dcs.ed.ac.uk/lfcs/research/types_bra/index.html),
+the [EC](http://www.lfcs.inf.ed.ac.uk/research/types-bra/index.html),
 and the [LFCS](http://www.lfcs.informatics.ed.ac.uk).
 
 David Aspinall designed the web pages and graphics for Proof General.

index.md

@@ -9,7 +9,7 @@ subtitle: A generic Emacs interface for proof assistants.
 **Proof General** is a generic front-end for *proof assistants* (also
 known as *interactive theorem provers*), based on the customizable text
 editor [Emacs](http://www.emacswiki.org). Proof General has been
-developed at the [LFCS](http://www.lfcs.informatics.ed.ac.uk/) in the
+developed at the [LFCS](http://wcms.inf.ed.ac.uk/lfcs/) in the
 [University of Edinburgh](http://www.ed.ac.uk/) with contributions from
 other sites. It is distributed under the conditions of the [GNU General
 Public License](http://www.gnu.org/licenses/gpl-2.0.html). The manager
@@ -26,10 +26,10 @@ Proof General offers a full support for latest versions of the Coq proof assista
 
 Proof General also supports previous versions of the following other proof assistants:
 
-- [![Isabelle logo](img/isabelle.png)](http://www.cl.cam.ac.uk/Research/HVG/Isabelle/)
+- [![Isabelle logo](img/isabelle.png)](http://www.cl.cam.ac.uk/research/hvg/Isabelle/)
   **Isabelle Proof General**,
-  for [Isabelle](http://www.cl.cam.ac.uk/Research/HVG/Isabelle/) (up to Isabelle2014)  
-  by [David Aspinall](http://homepages.inf.ed.ac.uk/da) and [Makarius](http://www.lri.fr/~wenzel).
+  for [Isabelle](http://www.cl.cam.ac.uk/research/hvg/Isabelle/) (up to Isabelle2014)  
+  by [David Aspinall](http://homepages.inf.ed.ac.uk/da) and [Makarius](http://sketis.net/).
 - [![PhoX logo](img/phox.png)](http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html)
   **PhoX Proof General**,
   for [PhoX](http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html)  

links.md

@@ -10,12 +10,11 @@ subtitle:
     Theorem Provers)](http://www.informatik.uni-bremen.de/uitp/)
     workshop series.
 -   [MathUI (Mathematical
-    User Interfaces)](http://www.activemath.org/workshops/MathUI/)
+    User Interfaces)](http://www.cermat.org/events/MathUI/)
     worshop series.
--   [ITP (Interactive
-    Theorem Proving)](http://itp2011.cs.ru.nl/ITP2011/Home.html)
+-   [ITP (Interactive Theorem Proving)](http://itp2016.inria.fr/)
     conference series (evolution/merger of
-    [TPHOLs](http://tphols.in.tum.de/) and others).
+    [TPHOLs](http://isabelle.in.tum.de/nominal/activities/tphols09/) and others).
 -   [MKM (Mathematical Knowledge Management)](http://www.mkm-ig.org/)
 
 ## Related Projects, Present and Past
@@ -28,7 +27,7 @@ subtitle:
     General-style interaction. It's perhaps in a more robust state than
     our own [Proof General Eclipse](http://proofgeneral.inf.ed.ac.uk/eclipse) prototype.
 -   As a possible foundation for generic proof environments,
-    [OpenMath](http://www.nag.co.uk/projects/openmath/omsoc/) is a
+    [OpenMath](http://www.openmath.org/society/) is a
     standard representation form for mathematical objects, which links
     in with the [MathML](http://www.w3.org/Math/) markup language.
 -   [Prosper](http://www.dcs.gla.ac.uk/prosper/) was a project to

pubs.md

@@ -31,7 +31,7 @@ subtitle: Papers about Proof General
     [pdf](http://proofgeneral.inf.ed.ac.uk/Kit/docs/pgipimp.pdf) (315k).
 -   [David Aspinall](http://homepages.inf.ed.ac.uk/da), [Christoph
     Lüth](http://www.informatik.uni-bremen.de/~cxl/) and [Burkhart
-    Wolff](http://www.infsec.ethz.ch/people/wolffb).
+    Wolff](https://www.lri.fr/~wolff/).
     ***Assisted Proof Document Authoring***.
     Appears in *Mathematical Knowledge Management 2005 (MKM '05)*,
     Springer LNAI 3863, p. 65--80, 2005.
@@ -57,28 +57,26 @@ subtitle: Papers about Proof General
 ## An Overview of Emacs Proof General
 
 -   [David Aspinall](http://homepages.inf.ed.ac.uk/da). [Proof General:
-    A Generic Tool for Proof Development](papers/pgoutline.ps.gz).
+    A Generic Tool for Proof Development](http://proofgeneral.inf.ed.ac.uk/papers/pgoutline.ps.gz).
     *Tools and Algorithms for the Construction and Analysis of Systems,
     Proc TACAS 2000*, LNCS 1785.
     Here are some [slides](http://proofgeneral.inf.ed.ac.uk/papers/pgtalk.pdf) used for this talk and
     some other presentations of Proof General.
 
 ## Related work and older documentation
 
--   [Yves Bertot](http://www-sop.inria.fr/lemme/Yves.Bertot) and
-    [Laurent
-    Théry](http://www.inria.fr/croap/personnel/Laurent.Thery/me.html).
+-   [Yves Bertot](http://www-sop.inria.fr/members/Yves.Bertot/index.html) and
+    [Laurent Théry](http://www-sop.inria.fr/marelle/personnel/Laurent.Thery/me.html).
     [A generic approach to building user interfaces for theorem
     provers](http://proofgeneral.inf.ed.ac.uk/papers/jsymcomp.ps.gz). *Journal of Symbolic Computation*,
     25(7), pp. 161-194, February 1998.
     This paper describes Script Management, also supported by
     Proof General.
-
 -   [Yves Bertot](http://www-sop.inria.fr/lemme/Yves.Bertot), Thomas
     Kleymann-Schreiber and Dilip Sequeira. *Implementing Proof by
     Pointing without a Structure Editor*. LFCS Technical Report
-    [ECS-LFCS-97-368](http://www.lfcs.informatics.ed.ac.uk/reports/97/ECS-LFCS-97-368/index.html).
-    Also published as Rapport de recherche de l'INRIA [Sophia
-    Antipolis](http://www.inria.fr/Unites/SOPHIA-eng.html)
-    [RR-3286](http://www.inria.fr/RRRT/RR-3286.html)
+    [ECS-LFCS-97-368](http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-368/index.html).
+    Also published as Rapport de recherche de
+    l'[Inria Sophia Antipolis](http://www.inria.fr/en/centre/sophia)
+    [RR-3286](https://hal.inria.fr/inria-00073402/).
     This paper describes PG's implementation of Proof by Pointing.