--- 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
--- 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 -->
--- 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).
--- 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> </li>
+<li> <a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/binary.html">Cambridge (UK)</a> <br> </li>
-<li> <a href="http://isabelle.in.tum.de/dist/source.html">Munich (Germany)</a> <br> </li>
+<li> <a href="http://isabelle.in.tum.de/dist/binary.html">Munich (Germany)</a> <br> </li>
-<li> <a href="http://ftp.research.bell-labs.com/dist/smlnj/isabelle/source.html">New Jersey (USA)</a> <br> </li>
+<li> <a href="http://ftp.research.bell-labs.com/dist/smlnj/isabelle/binary.html">New Jersey (USA)</a> <br> </li>
-<li> <a href="ftp://rodin.stanford.edu/pub/smlnj/isabelle/source.html">Stanford (USA)</a> <br> </li>
+<li> <a href="ftp://rodin.stanford.edu/pub/smlnj/isabelle/binary.html">Stanford (USA)</a> <br> </li>
</ul>
--- 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>
--- 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) -->