Updated web pages, misc improvements.

1 files changed, 41 insertions, 21 deletions

diff --git a/html/main.phtml b/html/main.phtml
index f0d07253..7844d527 100644
--- a/html/main.phtml
+++ b/html/main.phtml
@@ -13,7 +13,12 @@ works best under
 <a href="http://www.gnu.org/software/emacs/">FSF GNU Emacs</a>.
 You need a recent version in either case.
 </p>
-
+<p>
+The aim of the Proof General project is to provide a powerful and
+configurable interfaces which help user-interaction with interactive
+proof assistants.  The strategy of Proof General is to target power
+users rather than novices, but we include general user interface
+niceties, such as toolbar and menus, which make use easier for all.
 <p>
 To read more about what Proof General
 provides, 
@@ -27,7 +32,6 @@ To contact the developers, click
 </p>
 
 
-</p>
 
 <h2>What systems does Proof General work with?</h2>
 <p>
@@ -50,14 +54,35 @@ including:
          First crafted by 
          <a href="http://www.dcs.ed.ac.uk/~hhg">Healfdene Goguen</a>. 
 	 <br>
-	 Later contributions by Patrick Loiseleur.
+	 Contributions by Patrick Loiseleur.
          <br>
-	  Maintained by 
-	    <a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>.
+          Maintained by 
+	  <a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>.
         </div>
     </td>
  </tr>
  <tr>
+   <td align="center">
+       <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
+      "<img src=\"images/isabelle.gif\" width=74 height=64 border=0 alt=\"Isabelle badge\">",
+      "The Isabelle Home Page"); ?>
+   </td>
+   <td><b><?php fileshow("ProofGeneral/isa/README","Isabelle Proof General "); ?></b> for
+       <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
+		    "Isabelle", "The Isabelle Home Page"); ?>
+      <br>
+       <div style="font-size: smaller">
+       Crafted and maintained by 
+      <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+      <br>
+      Additional maintainance, support for
+      <a href="http://isabelle.in.tum.de/Isar">Isabelle/Isar</a>
+      by
+      <a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
+       </div>
+   </td>
+ </tr>
+ <tr>
     <td align="center">
        <?php hlink("http://www.dcs.ed.ac.uk/home/lego",
        "<img src=\"images/lego-badge.gif\" width=123 height=33 border=0 alt=\"LEGO badge\">",
@@ -73,32 +98,27 @@ including:
         <a href="http://www.dcs.ed.ac.uk/~djs/welcome.html">Dilip Sequeira</a>.
        <br>
        Maintained by 
-       <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>
+       <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>
        and
        <a href="http://www.dur.ac.uk/p.c.callaghan/">Paul Callaghan</a>.
        </div>
     </td>
  </tr>
  <tr>
-   <td align="center">
-       <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
-      "<img src=\"images/isabelle.gif\" width=74 height=64 border=0 alt=\"Isabelle badge\">",
-      "The Isabelle Home Page"); ?>
+    <td align="center">
+       <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html",
+       "AF2",
+       "The AF2 Home Page") ?>
    </td>
-   <td><b><?php fileshow("ProofGeneral/isa/README","Isabelle Proof General "); ?></b> for
-       <?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
-		    "Isabelle", "The Isabelle Home Page"); ?>
-      <br>
+    <td><b><?php fileshow("ProofGeneral/AF2/README","AF2 Proof General "); ?></b> for
+       <?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html",
+		   "AF2","The AF2 Home Page") ?>
+       <br>
        <div style="font-size: smaller">
        Crafted and maintained by 
-      <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>.
-      <br>
-      Additional maintainance, support for
-      <a href="http://isabelle.in.tum.de/Isar">Isabelle/Isar</a>
-      by
-      <a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
+       <a href="http://www.lama.univ-savoie.fr/~RAFFALLI">Christophe Raffalli</a>
        </div>
-   </td>
+    </td>
  </tr>
 </table>
 <p>