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 -->