# HG changeset patch
# User kleing
# Date 945875558 -3600
# Node ID dbbef2367723b303b25ae164415c295c51e1c232
# Parent  19b9f92ca503f522e508ebfd071bcf6b0c5b4a89
some tuning (incorporated David's suggestions)

diff -r 19b9f92ca503 -r dbbef2367723 Admin/page/dist-content/binary.content
--- a/Admin/page/dist-content/binary.content	Tue Dec 21 15:03:02 1999 +0100
+++ b/Admin/page/dist-content/binary.content	Wed Dec 22 16:12:38 1999 +0100
@@ -10,7 +10,7 @@
 <center>
 <table border="0" cellspacing="5" cellpadding="4" width="520">
 
-  <!-- _GP_ download("ML system", "rpm/smlnj-base-110.0.6-0.i386.rpm", "{RPM_SML_SIZE} K") -->
+  <!-- _GP_ download("ML system", "rpm/smlnj-110.0-3.i386.rpm", "{RPM_SML_SIZE} K") -->
   <!-- _GP_ download("Isabelle system", "rpm/isabelle.rpm", "{RPM_BASE_SIZE} K") -->
   <!-- _GP_ download("Isabelle/HOL image", "rpm/isabelle-HOL.i386.rpm", "{RPM_HOL_SIZE} K") -->
   <!-- _GP_ download("Isabelle/HOL-Real image (optional)", "rpm/isabelle-HOL-Real.i386.rpm", "{RPM_REAL_SIZE} K") -->
@@ -26,7 +26,12 @@
 Example installation procedure:
 
 <pre>
-rpm -i smlnj-base-110.0.6-0.i386.rpm
+rpm -i smlnj-base-110.0.3-0.i386.rpm
 rpm -i --prefix /usr/share isabelle.rpm             
 rpm -i --prefix /usr/share isabelle-HOL.i386.rpm    
 </pre>
+
+<p>
+
+Use the mailing list <a href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
+to discuss problems and results.  (Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?)
diff -r 19b9f92ca503 -r dbbef2367723 Admin/page/dist-content/index.content
--- a/Admin/page/dist-content/index.content	Tue Dec 21 15:03:02 1999 +0100
+++ b/Admin/page/dist-content/index.content	Wed Dec 22 16:12:38 1999 +0100
@@ -12,12 +12,12 @@
 
 <ul>	
 
-<li> <a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/">Cambridge (UK)</a> <br>&nbsp;</li>
+<li> <a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/source.html">Cambridge (UK)</a> <br>&nbsp;</li>
 
-<li> <a href="http://isabelle.in.tum.de/dist/">Munich (Germany)</a> <br>&nbsp;</li>
+<li> <a href="http://isabelle.in.tum.de/dist/source.html">Munich (Germany)</a> <br>&nbsp;</li>
 	
 
-<li> <a href="ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html">New Jersey (USA)</a> <br>&nbsp;</li>
+<li> <a href="ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/source.html">New Jersey (USA)</a> <br>&nbsp;</li>
 
 </ul>
 
diff -r 19b9f92ca503 -r dbbef2367723 Admin/page/dist-content/source.content
--- a/Admin/page/dist-content/source.content	Tue Dec 21 15:03:02 1999 +0100
+++ b/Admin/page/dist-content/source.content	Wed Dec 22 16:12:38 1999 +0100
@@ -22,3 +22,7 @@
 
 Please see the Isabelle <a href="{ISABELLE}/README.html">README</a> file for more information.
 
+<p>
+
+Use the mailing list <a href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
+to discuss problems and results.  (Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?)
diff -r 19b9f92ca503 -r dbbef2367723 Admin/page/main-content/index.content
--- a/Admin/page/main-content/index.content	Tue Dec 21 15:03:02 1999 +0100
+++ b/Admin/page/main-content/index.content	Wed Dec 22 16:12:38 1999 +0100
@@ -13,7 +13,7 @@
 
 <p>
 
-This page provides general information on Isabelle, more specific
+These pages provide <a href="about.html">general information on Isabelle</a>, more specific
 information is available from the local pages
 
 <ul>
@@ -38,12 +38,29 @@
 
 The current version is <strong>{ISABELLE}</strong>.  Several mirror
 sites provide the Isabelle <a href="dist/">distribution</a>, which
-includes sources, documentation, and binary packages.
-
+includes <a href="dist/source.html">sources</a>, 
+<a href="dist/binary.html">binary packages</a>, and 
+<a href="dist/docs.html">documentation</a>.
 
 <p>
 &nbsp;
 
+<h2>User interface</h2>
+
+The distribution includes only a very primitive interface based on
+ordinary terminal sessions.
+
+<p>
+
+<a href="http://zermelo.dcs.ed.ac.uk/~proofgen/">Proof General</a> is
+a generic Emacs interface for proof assistants, including Isabelle
+(both for the classic and Isar version).  Proof General is suitable
+for use by pacifists and Emacs militants alike. Its most prominent
+feature is script management, providing a metaphor of <em>live proof
+script editing</em>.
+
+<p>
+&nbsp;
 
 <h2>Mailing list</h2>
 
diff -r 19b9f92ca503 -r dbbef2367723 Admin/page/main-layout/navigation.html
--- a/Admin/page/main-layout/navigation.html	Tue Dec 21 15:03:02 1999 +0100
+++ b/Admin/page/main-layout/navigation.html	Wed Dec 22 16:12:38 1999 +0100
@@ -9,7 +9,7 @@
 <!-- _GP_ setnavcolor("#F0F0F0") -->
 <!-- _GP_ page("Home", "index") -->
 <!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("About", "about") -->
+<!-- _GP_ page("Isabelle?", "about") -->
 <!-- _GP_ empty_line(3) -->
 <!-- _GP_ page("Documentation", "docs") -->
 <!-- _GP_ empty_line(3) -->