# HG changeset patch
# User kleing
# Date 1082369878 -7200
# Node ID 4a9cc3080dbcc37e0ff8e26e97ed7661661cd653
# Parent  96bcf6d0bf721ee580e3d6bfb5ac3c6bde6c5620
inlcude HOL proof terms and HOL4 image

diff -r 96bcf6d0bf72 -r 4a9cc3080dbc Admin/page/dist-content/packages.content
--- a/Admin/page/dist-content/packages.content	Mon Apr 19 12:12:01 2004 +0200
+++ b/Admin/page/dist-content/packages.content	Mon Apr 19 12:17:58 2004 +0200
@@ -30,15 +30,17 @@
 <h2>Packages</h2>
 
 We provide a complete set of packages for Isabelle, Proof General, and
-PolyML.  The Proof General package contains a development snapshot
-that works well with <!-- _GP_ distname -->. We will update it to the
-newest stable version as soon as it is released.
-
+PolyML.  
+<p>
 While XEmacs-21 is not included here, most operating system
 distributions already provide a suitable package, although not
 installed by default.  Some of the packages below are platform
 dependent; we include binaries for Linux/x86, Solaris/Sparc, and
-Darwin/PPC (MacOS X).
+Darwin/PPC (MacOS X). 
+<p>
+Short <a href="#install">installation instructions</a> are near the
+bottom of this page. For more information, see the file INSTALL in
+<!-- _GP_ distname -->.tar.gz.
 
 <p>
 
@@ -53,7 +55,7 @@
 <!-- _GP_ download(1, "Theory library in PDF and HTML", distname . "_library.tar.gz", "../..") -->
 
 <!-- _GP_ downloadhead("Proof General") -->
-<!-- _GP_ download(1, "Proof General", "contrib/ProofGeneral.tar.gz", "../..") -->
+<!-- _GP_ download(1, "Proof General", "contrib/ProofGeneral-3.5.tar.gz", "../..") -->
 
 <!-- _GP_ downloadhead("Poly/ML compiler and runtime system") -->
 <!-- _GP_ download(1, "Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") -->
@@ -68,10 +70,16 @@
 <!-- _GP_ download(3, "HOL-Complex", "HOL-Complex_x86-linux.tar.gz", "../..") -->
 <!-- _GP_ download(0, "", "HOL-Complex_sparc-solaris.tar.gz", "../..") -->
 <!-- _GP_ download(0, "", "HOL-Complex_ppc-darwin.tar.gz", "../..") -->
+<!-- _GP_ download(3, "HOL4", "HOL4_x86-linux.tar.gz", "../..") -->
+<!-- _GP_ download(0, "", "HOL4_sparc-solaris.tar.gz", "../..") -->
+<!-- _GP_ download(0, "", "HOL4_ppc-darwin.tar.gz", "../..") -->
 <!-- _GP_ download(3, "ZF", "ZF_x86-linux.tar.gz", "../..") -->
 <!-- _GP_ download(0, "", "ZF_sparc-solaris.tar.gz", "../..") -->
 <!-- _GP_ download(0, "", "ZF_ppc-darwin.tar.gz", "../..") -->
 
+<!-- _GP_ downloadhead("HOL4 proof terms") -->
+<!-- _GP_ download(1, "HOL4 proof terms", "contrib/HOL4-proofs.tar.gz", "../..") -->
+
 </table>
 </center>
 
@@ -79,7 +87,7 @@
 
 <h2>Installation</h2>
 
-In fact, there is no installation required.  Users may just unpack all
+<a name="install">In</a> 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.