--- a/Admin/page/dist-content/packages.content Fri Jan 11 17:04:49 2002 +0100
+++ b/Admin/page/dist-content/packages.content Fri Jan 11 18:07:30 2002 +0100
@@ -36,11 +36,10 @@
<p>
-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.
+Some of the packages below are platform dependent. We include binary
+packages for Linux/x86, Solaris/Sparc, and Darwin/PPC (MacOS X).
+Isabelle also works with different Standard ML implementations (and
+further platforms).
<p>
@@ -49,29 +48,31 @@
<table border="0" cellspacing="5" cellpadding="4" width="520">
-<!-- _GP_ downloadhead("Isabelle system") -->
+<!-- _GP_ downloadhead("Isabelle") -->
<!-- _GP_ download(1, "Main sources and documentation", distname . ".tar.gz", "../..") -->
<!-- _GP_ download(1, "Alternative documentation in PDF", distname . "_pdf.tar.gz", "../..") -->
<!-- _GP_ download(1, "Browsable version of theory library", distname . "_library.tar.gz", "../..") -->
+<!-- _GP_ downloadhead("Proof General") -->
+<!-- _GP_ download(1, "Proof General", "contrib/ProofGeneral.tar.gz", "../..") -->
+<!-- _GP_ download(1, "X-Symbol package", "contrib/x-symbol.tar.gz", "../..") -->
+
<!-- _GP_ downloadhead("Poly/ML compiler and runtime system") -->
<!-- _GP_ download(1, "Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") -->
-<!-- _GP_ download(4, "Poly/ML binary modules", "contrib/polyml_x86-linux.tar.gz", "../..") -->
+<!-- _GP_ download(3, "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", "../..") -->
+<!-- _GP_ downloadhead("Precompiled logics") -->
+<!-- _GP_ download(3, "HOL", "HOL_x86-linux.tar.gz", "../..") -->
<!-- _GP_ download(0, "", "HOL_sparc-solaris.tar.gz", "../..") -->
-<!-- _GP_ download(2, "HOL-Real", "HOL-Real_x86-linux.tar.gz", "../..") -->
+<!-- _GP_ download(0, "", "HOL_ppc-darwin.tar.gz", "../..") -->
+<!-- _GP_ download(3, "HOL-Real", "HOL-Real_x86-linux.tar.gz", "../..") -->
<!-- _GP_ download(0, "", "HOL-Real_sparc-solaris.tar.gz", "../..") -->
-<!-- _GP_ download(2, "ZF", "ZF_x86-linux.tar.gz", "../..") -->
+<!-- _GP_ download(0, "", "HOL-Real_ppc-darwin.tar.gz", "../..") -->
+<!-- _GP_ download(3, "ZF", "ZF_x86-linux.tar.gz", "../..") -->
<!-- _GP_ download(0, "", "ZF_sparc-solaris.tar.gz", "../..") -->
-
-<!-- _GP_ downloadhead("Proof General system") -->
-<!-- _GP_ download(1, "Proof General", "contrib/ProofGeneral.tar.gz", "../..") -->
-<!-- _GP_ download(1, "X-Symbol package", "contrib/x-symbol.tar.gz", "../..") -->
+<!-- _GP_ download(0, "", "ZF_ppc-darwin.tar.gz", "../..") -->
</table>
</center>
@@ -80,9 +81,9 @@
<h2>Installation</h2>
-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.
+In fact, 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>
@@ -97,15 +98,15 @@
tar -C /usr/local -xzf
<!-- _GP_ href(distname . ".tar.gz", distname . ".tar.gz") --> <br>
tar -C /usr/local -xzf
+<!-- _GP_ href("contrib/ProofGeneral.tar.gz", "ProofGeneral.tar.gz") --> <br>
+ tar -C /usr/local -xzf
+<!-- _GP_ href("contrib/x-symbol.tar.gz", "x-symbol.tar.gz") --> <br>
+ tar -C /usr/local -xzf
<!-- _GP_ href("contrib/polyml_base.tar.gz", "polyml_base.tar.gz") --> <br>
tar -C /usr/local -xzf
<!-- _GP_ href("contrib/polyml_x86-linux.tar.gz", "polyml_x86-linux.tar.gz") --> <br>
tar -C /usr/local -xzf
<!-- _GP_ href("HOL_x86-linux.tar.gz", "HOL_x86-linux.tar.gz") --> <br>
- tar -C /usr/local -xzf
-<!-- _GP_ href("contrib/ProofGeneral.tar.gz", "ProofGeneral.tar.gz") --> <br>
- tar -C /usr/local -xzf
-<!-- _GP_ href("contrib/x-symbol.tar.gz", "x-symbol.tar.gz") --> <br>
</tt>
<p>