1.1 --- a/Admin/page/main-content/index.content	Tue Dec 21 15:03:02 1999 +0100
     1.2 +++ b/Admin/page/main-content/index.content	Wed Dec 22 16:12:38 1999 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  <p>
     1.6  
     1.7 -This page provides general information on Isabelle, more specific
     1.8 +These pages provide <a href="about.html">general information on Isabelle</a>, more specific
     1.9  information is available from the local pages
    1.10  
    1.11  <ul>
    1.12 @@ -38,12 +38,29 @@
    1.13  
    1.14  The current version is <strong>{ISABELLE}</strong>.  Several mirror
    1.15  sites provide the Isabelle <a href="dist/">distribution</a>, which
    1.16 -includes sources, documentation, and binary packages.
    1.17 -
    1.18 +includes <a href="dist/source.html">sources</a>, 
    1.19 +<a href="dist/binary.html">binary packages</a>, and 
    1.20 +<a href="dist/docs.html">documentation</a>.
    1.21  
    1.22  <p>
    1.23  &nbsp;
    1.24  
    1.25 +<h2>User interface</h2>
    1.26 +
    1.27 +The distribution includes only a very primitive interface based on
    1.28 +ordinary terminal sessions.
    1.29 +
    1.30 +<p>
    1.31 +
    1.32 +<a href="http://zermelo.dcs.ed.ac.uk/~proofgen/">Proof General</a> is
    1.33 +a generic Emacs interface for proof assistants, including Isabelle
    1.34 +(both for the classic and Isar version).  Proof General is suitable
    1.35 +for use by pacifists and Emacs militants alike. Its most prominent
    1.36 +feature is script management, providing a metaphor of <em>live proof
    1.37 +script editing</em>.
    1.38 +
    1.39 +<p>
    1.40 +&nbsp;
    1.41  
    1.42  <h2>Mailing list</h2>
    1.43