# HG changeset patch
# User wenzelm
# Date 1001427466 -7200
# Node ID 1ce3771d2b492e0d4aa48e8f6462a6d06d7a653e
# Parent  b6a181110c3c08fa47d08c6896d0ca9152d9c46e
updated;

diff -r b6a181110c3c -r 1ce3771d2b49 Admin/page/dist-content/packages.content
--- a/Admin/page/dist-content/packages.content	Tue Sep 25 14:19:29 2001 +0200
+++ b/Admin/page/dist-content/packages.content	Tue Sep 25 16:17:46 2001 +0200
@@ -14,11 +14,12 @@
 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. <a
-href="http://www.polyml.org">Poly/ML</a> as provided below).  A
+href="http://www.polyml.org">Poly/ML</a> as included below).  A
 <em>comfortable</em> Isabelle working environment demands further user
 interface support, as provided by <a
-href="http://www.proofgeneral.org">Proof General</a> together with the
-(optional) <a
+href="http://www.proofgeneral.org">Proof General</a> (please <a
+href="http://www.proofgeneral.org/register">register</a>) together
+with the (optional) <a
 href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>
 package.  Both of these should be used with a recent version of <a
 href="http://www.xemacs.org">XEmacs-21</a>.
@@ -35,10 +36,11 @@
 
 <p>
 
-Some packages are platform dependent.  Everything is included below
-for Linux/x86 and Solaris/Sparc systems.  Other Unix platforms work as
-well, but require manual compilation of Isabelle logic images using a
-suitable Standard ML system.
+Some of the packages below are platform dependent.  We include a
+complete binary distribution for Linux/x86 and Solaris/Sparc systems;
+the PowerPC platform requires separate compilation of Isabelle logic
+images.  Isabelle also works with different Standard ML
+implementations (for further platforms) not included here.
 
 <p>
 
@@ -53,8 +55,10 @@
 
 <!-- _GP_ downloadhead("Poly/ML compiler and runtime system") -->
 <!-- _GP_ download(1, "Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") -->
-<!-- _GP_ download(2, "Poly/ML binary modules", "contrib/polyml_x86-linux.tar.gz", "../..") -->
+<!-- _GP_ download(4, "Poly/ML binary modules", "contrib/polyml_x86-linux.tar.gz", "../..") -->
 <!-- _GP_ download(0, "", "contrib/polyml_sparc-solaris.tar.gz", "../..") -->
+<!-- _GP_ download(0, "", "contrib/polyml_ppc-linux.tar.gz", "../..") -->
+<!-- _GP_ download(0, "", "contrib/polyml_ppc-darwin.tar.gz", "../..") -->
 
 <!-- _GP_ downloadhead("Precompiled Isabelle logics") -->
 <!-- _GP_ download(2, "HOL", "HOL_x86-linux.tar.gz", "../..") -->
@@ -75,17 +79,16 @@
 
 <h2>Installation</h2>
 
-Installation is very easy.  Basically, just unpack all required
-packages within the same directory.  There is <em>no</em> manual
-configuration required of any of these components, if used according
-to the default settings of Isabelle.
+Actually there is no ``installation'' required, users may just unpack
+all required packages within the same directory.  The default settings
+of Isabelle should be reasonable for most circumstances.
 
 <p>
 
-A typical Linux/x86 site installation of Isabelle/HOL works as
-follows.  By using GNU <tt>tar</tt>, the archives are uncompressed and
-unpacked into the <tt>/usr/local</tt> directory (this location may be
-changed to anything appropriate).
+A typical Linux/x86 site installation of Isabelle/HOL would be
+arranged as follows.  By using GNU <tt>tar</tt>, the archives are
+uncompressed and unpacked into the <tt>/usr/local</tt> directory (this
+location may be changed to anything appropriate).
 
 <p>