# HG changeset patch
# User wenzelm
# Date 969221708 -7200
# Node ID ede5f78b939853781b66db804f8c226a33dc5033
# Parent  8cd7ef5b8f9df197f6233ed9cc5a91f69f614bad
tuned;

diff -r 8cd7ef5b8f9d -r ede5f78b9398 Admin/page/Contents
--- a/Admin/page/Contents	Sun Sep 17 13:51:37 2000 +0200
+++ b/Admin/page/Contents	Sun Sep 17 22:15:08 2000 +0200
@@ -1,1 +1,1 @@
-dummy	Dummy Isabelle documentation entry.
+dummy	Dummy Isabelle documentation entry
diff -r 8cd7ef5b8f9d -r ede5f78b9398 Admin/page/dist-content/binary.content
--- a/Admin/page/dist-content/binary.content	Sun Sep 17 13:51:37 2000 +0200
+++ b/Admin/page/dist-content/binary.content	Sun Sep 17 22:15:08 2000 +0200
@@ -5,17 +5,46 @@
 
 <p>
 
-<strong>NOTE.</strong> The binary distribution is designed for easy
-installation of Isabelle, and related tools such as Proof General and
-X-Symbol.  There is no manual intervention required, provided that the
-versions of packages as provided below are used.
+The binary distribution of <!-- _GP_ distname --> provides everything
+required for easy installation of the full Isabelle working
+environment on common Unix platforms.
+
+<p>
+
+A <em>minimal</em> Isabelle installation requires only <tt>bash</tt>
+and <tt>perl</tt> (usually provided by the operating system), and a
+suitable implementation of Standard ML (e.g. Poly/ML as provided
+below).
+
+<p>
+
+A <em>comfortable</em> Isabelle working environment demands further
+user interface support, as provided by <a
+href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a>
+together with the (optional) <a
+href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>
+package.  Both of these require a recent version of <a
+href="http://www.xemacs.org">XEmacs</a> (e.g. version 21).
+
+<p>
+
+Below we offer tuned distributions of Proof General and X-Symbol, such
+that <em>no manual configuration</em> is required when used with
+Isabelle.  (In case that the original distributions are used instead,
+refer to their included instructions for installation details.)  Note
+that XEmacs-21 is not included here -- most operating system
+distributions already provide suitable packages, although not
+installed by default.
+
+<p>
 
 
 <h2>(1) Linux/x86 systems with RPM</h2>
 
-This is the binary distribution of <!-- _GP_ distname --> for
-Linux/x86 systems.  It requires RPM based package management (as used
-by most Linux distributions), and root user access to install.
+This version of the <!-- _GP_ distname --> binary distribution is for
+Linux/x86 systems with RPM package management, as used by most Linux
+distributions.  Note that <tt>rpm</tt> requires root user access for
+installation.
 
 <p>
 
@@ -41,7 +70,7 @@
 rpm -i --prefix /usr/share polyml.i386.rpm
 rpm -i --prefix /usr/share isabelle.rpm
 rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
-rpm -i --prefix /usr/share proofgeneral.rpm               #requires XEmacs-21
+rpm -i --prefix /usr/share proofgeneral.rpm
 rpm -i --prefix /usr/share xsymbol.rpm
 </pre>
 
@@ -50,8 +79,8 @@
 
 <h2>(2) Generic Linux/x86 or Solaris/Sparc systems</h2>
 
-The following distribution of <!-- _GP_ distname --> works for any
-Linux/x86 or Solaris/Sparc system -- only Poly/ML is platform
+The following <!-- _GP_ distname --> binary distribution works for any
+Linux/x86 or Solaris/Sparc system -- actually only Poly/ML is platform
 dependent.  Installation does not rely on package management; it may
 be performed by non-root users as well.
 
@@ -77,7 +106,7 @@
 tar -C /usr/local -x -z -f polyml_base.tar.gz
 tar -C /usr/local -x -z -f polyml_x86-linux.tar.gz
 tar -C /usr/local -x -z -f <!-- _GP_ distname . ".tar.gz"-->
-tar -C /usr/local -x -z -f ProofGeneral.tar.gz            #requires XEmacs-21
+tar -C /usr/local -x -z -f ProofGeneral.tar.gz
 tar -C /usr/local -x -z -f x-symbol.tar.gz
 
 cd <!-- _GP_ "/usr/local/" . distname -->
diff -r 8cd7ef5b8f9d -r ede5f78b9398 Admin/page/dist-content/docs.content
--- a/Admin/page/dist-content/docs.content	Sun Sep 17 13:51:37 2000 +0200
+++ b/Admin/page/dist-content/docs.content	Sun Sep 17 22:15:08 2000 +0200
@@ -2,9 +2,8 @@
 Isabelle Documentation
 
 %body%
-The Isabelle documentation:
+<!-- _GP_ distname --> documentation is included here as browsable PDF
+for convenience.  These documents are also part of the standard
+Isabelle distribution.
 
 <!-- _GP_ include("$pwd/docu-contents.dist") -->
-
-All this documentation is also part of the Isabelle distribution (both
-as dvi and pdf).
diff -r 8cd7ef5b8f9d -r ede5f78b9398 Admin/page/dist-content/index.content
--- a/Admin/page/dist-content/index.content	Sun Sep 17 13:51:37 2000 +0200
+++ b/Admin/page/dist-content/index.content	Sun Sep 17 22:15:08 2000 +0200
@@ -12,12 +12,12 @@
 
 <ul>	
 
-<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://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/binary.html">Cambridge (UK)</a> <br>&nbsp;</li>
 
-<li> <a href="http://isabelle.in.tum.de/dist/source.html">Munich (Germany)</a> <br>&nbsp;</li>
+<li> <a href="http://isabelle.in.tum.de/dist/binary.html">Munich (Germany)</a> <br>&nbsp;</li>
 	
-<li> <a href="http://ftp.research.bell-labs.com/dist/smlnj/isabelle/source.html">New Jersey (USA)</a> <br>&nbsp;</li>
+<li> <a href="http://ftp.research.bell-labs.com/dist/smlnj/isabelle/binary.html">New Jersey (USA)</a> <br>&nbsp;</li>
 
-<li> <a href="ftp://rodin.stanford.edu/pub/smlnj/isabelle/source.html">Stanford (USA)</a> <br>&nbsp;</li>
+<li> <a href="ftp://rodin.stanford.edu/pub/smlnj/isabelle/binary.html">Stanford (USA)</a> <br>&nbsp;</li>
 
 </ul>
diff -r 8cd7ef5b8f9d -r ede5f78b9398 Admin/page/dist-content/source.content
--- a/Admin/page/dist-content/source.content	Sun Sep 17 13:51:37 2000 +0200
+++ b/Admin/page/dist-content/source.content	Sun Sep 17 22:15:08 2000 +0200
@@ -2,7 +2,9 @@
 Isabelle Source Distribution
 
 %body%
-This is the complete source distribution of <!-- _GP_ distname -->.
+This is the pure source distribution of <!-- _GP_ distname -->.  Note
+that the <a href="binary.html">binary distribution</a> includes all
+Isabelle sources as well.
 
 <p>
 
@@ -19,10 +21,10 @@
 
 <p>
 
-Please see the Isabelle <!-- _GP_ href(distname . "/README.html",
-"README") --> and <!-- _GP_ href(distname . "/INSTALL", "INSTALL") -->
-files for more information.  See the <!-- _GP_ href(distname
-. "/NEWS", "NEWS") --> file for a history user-relevant changes.
+See the Isabelle <!-- _GP_ href(distname . "/README.html", "README")
+--> and <!-- _GP_ href(distname . "/INSTALL", "INSTALL") --> files for
+more information.  See the <!-- _GP_ href(distname . "/NEWS", "NEWS")
+--> file for a history user-relevant changes.
 
 <p>
 
diff -r 8cd7ef5b8f9d -r ede5f78b9398 Admin/page/dist-layout/navigation.html
--- a/Admin/page/dist-layout/navigation.html	Sun Sep 17 13:51:37 2000 +0200
+++ b/Admin/page/dist-layout/navigation.html	Sun Sep 17 22:15:08 2000 +0200
@@ -12,9 +12,9 @@
 <!-- _GP_ setnavcolor("#F0F0F0") -->
 <!-- _GP_ page("Mirrors", "index") -->
 <!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("Sources", "source") -->
+<!-- _GP_ page("Binaries", "binary") -->
 <!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("Binaries", "binary") -->
+<!-- _GP_ page("Sources", "source") -->
 <!-- _GP_ empty_line(3) -->
 <!-- _GP_ page("Documentation", "docs") -->
 <!-- _GP_ empty_line(3) -->