# HG changeset patch
# User wenzelm
# Date 969280554 -7200
# Node ID 3833b58a5d8847bb0e68a2863470b824c654c2b8
# Parent  8c16ec5ba62bad329ecd42d54a61e46f19c0d27e
improved pages;

diff -r 8c16ec5ba62b -r 3833b58a5d88 Admin/page/dist-content/binary.content
--- a/Admin/page/dist-content/binary.content	Mon Sep 18 14:10:31 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,120 +0,0 @@
-%title%
-Isabelle Binary Distribution
-
-%body%
-
-<p>
-
-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 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>
-
-<!-- _GP_ setdowncolor("#E0E0E0") -->
-<center>
-<table border="0" cellspacing="5" cellpadding="4" width="520">
-  <!-- _GP_ download("Poly/ML system", "contrib/polyml.i386.rpm", "../..") -->
-  <!-- _GP_ download("Isabelle main system", "isabelle.rpm", "../..") -->
-  <!-- _GP_ download("Isabelle/HOL image", "isabelle-HOL.i386.rpm", "../..") -->
-  <!-- _GP_ download("Isabelle/HOL-Real image (optional)", "isabelle-HOL-Real.i386.rpm", "../..") -->
-  <!-- _GP_ download("Isabelle/ZF image (optional)", "isabelle-ZF.i386.rpm", "../..") -->
-  <!-- _GP_ download("Isabelle pdf documentation (optional)", "isabelle-pdfdocs.rpm", "../..") -->
-  <!-- _GP_ download("Proof General system (recommended)", "contrib/proofgeneral.rpm", "../..") -->
-  <!-- _GP_ download("X-Symbol package (recommended)", "contrib/xsymbol.rpm", "../..") -->
-</table>
-</center>
-
-<p>
-
-Example installation in <tt>/usr/share</tt> (the default location):
-
-<pre>
-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
-rpm -i --prefix /usr/share xsymbol.rpm
-</pre>
-
-<p>
-
-
-<h2>(2) Generic Linux/x86 or Solaris/Sparc systems</h2>
-
-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.
-
-<p>
-
-<!-- _GP_ setdowncolor("#E0E0E0") -->
-<center>
-<table border="0" cellspacing="5" cellpadding="4" width="520">
-  <!-- _GP_ download("Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") -->
-  <!-- _GP_ download("Poly/ML module for Linux/x86", "contrib/polyml_x86-linux.tar.gz", "../..") -->
-  <!-- _GP_ download("Poly/ML module for Solaris/Sparc", "contrib/polyml_sparc-solaris.tar.gz", "../..") -->
-  <!-- _GP_ download("Isabelle main system", distname . ".tar.gz", "../..") -->
-  <!-- _GP_ download("Isabelle pdf documentation (optional)", distname . "_pdf.tar.gz", "../..") -->  <!-- _GP_ download("Proof General system (recommended)", "contrib/ProofGeneral.tar.gz", "../..") -->
-  <!-- _GP_ download("X-Symbol package (recommended)", "contrib/x-symbol.tar.gz", "../..") -->
-</table>
-</center>
-
-<p>
-
-Example installation in <tt>/usr/local</tt> for Linux/x86:
-
-<pre>
-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
-tar -C /usr/local -x -z -f x-symbol.tar.gz
-
-cd <!-- _GP_ "/usr/local/" . distname -->
-./configure
-./build
-./bin/isatool install -p /usr/local/bin
-</pre>
-
-<p>
-
-<p>
diff -r 8c16ec5ba62b -r 3833b58a5d88 Admin/page/dist-content/docs.content
--- a/Admin/page/dist-content/docs.content	Mon Sep 18 14:10:31 2000 +0200
+++ b/Admin/page/dist-content/docs.content	Mon Sep 18 14:35:54 2000 +0200
@@ -7,3 +7,12 @@
 Isabelle distribution.
 
 <!-- _GP_ include("$pwd/docu-contents.dist") -->
+
+The following text files of the Isabelle distribution may be of some
+interest:
+<ul>
+<li> <!-- _GP_ href(distname . "/ANNOUNCE", "ANNOUNCE") -->
+<li> <!-- _GP_ href(distname . "/README.html", "README") -->
+<li> <!-- _GP_ href(distname . "/INSTALL", "INSTALL") -->
+<li> <!-- _GP_ href(distname . "/NEWS", "NEWS") -->
+</ul>
diff -r 8c16ec5ba62b -r 3833b58a5d88 Admin/page/dist-content/index.content
--- a/Admin/page/dist-content/index.content	Mon Sep 18 14:10:31 2000 +0200
+++ b/Admin/page/dist-content/index.content	Mon Sep 18 14:35:54 2000 +0200
@@ -4,7 +4,6 @@
 %title%
 Isabelle Distribution Area
 
-
 %body%
 <p>
 
@@ -12,12 +11,19 @@
 
 <ul>	
 
-<li> <a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/binary.html">Cambridge (UK)</a> <br>&nbsp;</li>
+<li> <a
+href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/packages.html">Cambridge
+(UK)</a> <br>&nbsp;</li>
 
-<li> <a href="http://isabelle.in.tum.de/dist/binary.html">Munich (Germany)</a> <br>&nbsp;</li>
+<li> <a href="http://isabelle.in.tum.de/dist/packages.html">Munich
+(Germany)</a> <br>&nbsp;</li>
 	
-<li> <a href="http://ftp.research.bell-labs.com/dist/smlnj/isabelle/binary.html">New Jersey (USA)</a> <br>&nbsp;</li>
+<li> <a
+href="http://ftp.research.bell-labs.com/dist/smlnj/isabelle/packages.html">New
+Jersey (USA)</a> <br>&nbsp;</li>
 
-<li> <a href="ftp://rodin.stanford.edu/pub/smlnj/isabelle/binary.html">Stanford (USA)</a> <br>&nbsp;</li>
+<li> <a
+href="ftp://rodin.stanford.edu/pub/smlnj/isabelle/packages.html">Stanford
+(USA)</a> <br>&nbsp;</li>
 
 </ul>
diff -r 8c16ec5ba62b -r 3833b58a5d88 Admin/page/dist-content/packages.content
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/dist-content/packages.content	Mon Sep 18 14:35:54 2000 +0200
@@ -0,0 +1,120 @@
+%title%
+Isabelle Packages
+
+%body%
+
+<p>
+
+The following source and binary packages of <!-- _GP_ distname -->
+provide 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 version of the <!-- _GP_ distname --> 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>
+
+<!-- _GP_ setdowncolor("\"#E0E0E0\"") -->
+<center>
+<table border="0" cellspacing="5" cellpadding="4" width="520">
+  <!-- _GP_ download("Poly/ML system", "contrib/polyml.i386.rpm", "../..") -->
+  <!-- _GP_ download("Isabelle main system", "isabelle.rpm", "../..") -->
+  <!-- _GP_ download("Isabelle/HOL image", "isabelle-HOL.i386.rpm", "../..") -->
+  <!-- _GP_ download("Isabelle/HOL-Real image (optional)", "isabelle-HOL-Real.i386.rpm", "../..") -->
+  <!-- _GP_ download("Isabelle/ZF image (optional)", "isabelle-ZF.i386.rpm", "../..") -->
+  <!-- _GP_ download("Isabelle pdf documentation (optional)", "isabelle-pdfdocs.rpm", "../..") -->
+  <!-- _GP_ download("Proof General system (recommended)", "contrib/proofgeneral.rpm", "../..") -->
+  <!-- _GP_ download("X-Symbol package (recommended)", "contrib/xsymbol.rpm", "../..") -->
+</table>
+</center>
+
+<p>
+
+Example installation in <tt>/usr/share</tt> (the default location):
+
+<pre>
+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
+rpm -i --prefix /usr/share xsymbol.rpm
+</pre>
+
+<p>
+
+
+<h2>(2) Generic Linux/x86 or Solaris/Sparc systems</h2>
+
+The following <!-- _GP_ distname --> 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.
+
+<p>
+
+<!-- _GP_ setdowncolor("\"#E0E0E0\"") -->
+<center>
+<table border="0" cellspacing="5" cellpadding="4" width="520">
+  <!-- _GP_ download("Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") -->
+  <!-- _GP_ download("Poly/ML module for Linux/x86", "contrib/polyml_x86-linux.tar.gz", "../..") -->
+  <!-- _GP_ download("Poly/ML module for Solaris/Sparc", "contrib/polyml_sparc-solaris.tar.gz", "../..") -->
+  <!-- _GP_ download("Isabelle main system", distname . ".tar.gz", "../..") -->
+  <!-- _GP_ download("Isabelle pdf documentation (optional)", distname . "_pdf.tar.gz", "../..") -->  <!-- _GP_ download("Proof General system (recommended)", "contrib/ProofGeneral.tar.gz", "../..") -->
+  <!-- _GP_ download("X-Symbol package (recommended)", "contrib/x-symbol.tar.gz", "../..") -->
+</table>
+</center>
+
+<p>
+
+Example installation in <tt>/usr/local</tt> for Linux/x86:
+
+<pre>
+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
+tar -C /usr/local -x -z -f x-symbol.tar.gz
+
+cd <!-- _GP_ "/usr/local/" . distname -->
+./configure
+./build
+./bin/isatool install -p /usr/local/bin
+</pre>
+
+<p>
+
+<p>
diff -r 8c16ec5ba62b -r 3833b58a5d88 Admin/page/dist-content/source.content
--- a/Admin/page/dist-content/source.content	Mon Sep 18 14:10:31 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-%title%
-Isabelle Source Distribution
-
-%body%
-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>
-
-<!-- _GP_ setdowncolor("#E0E0E0") -->
-
-<center>
-<table border="0" cellspacing="5" cellpadding="4" width="500">
-
-  <!-- _GP_ download("Isabelle sources with dvi documentation", distname . ".tar.gz", "../..") -->
-  <!-- _GP_ download("Documentation as pdf files", distname . "_pdf.tar.gz", "../..") -->
-
-</table>
-</center>
-
-<p>
-
-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>
-
-Use the mailing list <a
-href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
-to discuss problems and results.  Why not <a
-href="mailto:lcp@cl.cam.ac.uk">subscribe</a>?
diff -r 8c16ec5ba62b -r 3833b58a5d88 Admin/page/dist-layout/navigation.html
--- a/Admin/page/dist-layout/navigation.html	Mon Sep 18 14:10:31 2000 +0200
+++ b/Admin/page/dist-layout/navigation.html	Mon Sep 18 14:35:54 2000 +0200
@@ -12,9 +12,7 @@
 <!-- _GP_ setnavcolor("#F0F0F0") -->
 <!-- _GP_ page("Mirrors", "index") -->
 <!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("Binaries", "binary") -->
-<!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("Sources", "source") -->
+<!-- _GP_ page("Packages", "packages") -->
 <!-- _GP_ empty_line(3) -->
 <!-- _GP_ page("Documentation", "docs") -->
 <!-- _GP_ empty_line(3) -->
diff -r 8c16ec5ba62b -r 3833b58a5d88 Admin/page/dist-layout/template.html
--- a/Admin/page/dist-layout/template.html	Mon Sep 18 14:10:31 2000 +0200
+++ b/Admin/page/dist-layout/template.html	Mon Sep 18 14:35:54 2000 +0200
@@ -15,7 +15,7 @@
 
   <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
 
-    <table border="0" cellspacing="5" width="100%" height="100%">
+    <table border="0" cellspacing="5" width="100%">
 
       <tr>
         <td width="20%" valign="top" bgcolor="#D8D8FF"> 
diff -r 8c16ec5ba62b -r 3833b58a5d88 Admin/page/main-content/docs.content
--- a/Admin/page/main-content/docs.content	Mon Sep 18 14:10:31 2000 +0200
+++ b/Admin/page/main-content/docs.content	Mon Sep 18 14:35:54 2000 +0200
@@ -3,7 +3,8 @@
 
 %body%
 
-<!-- _GP_ include("$pwd/docu-contents.main") -->
+<!-- _GP_ distname --> documentation is included here as browsable PDF
+for convenience.  These documents are also part of the standard
+Isabelle <a href="dist/">distribution</a>.
 
-All this documentation is also part of the Isabelle <a
-href="dist/">distribution</a> (both as dvi and pdf).
+<!-- _GP_ include("$pwd/docu-contents.main") -->
diff -r 8c16ec5ba62b -r 3833b58a5d88 Admin/page/main-content/index.content
--- a/Admin/page/main-content/index.content	Mon Sep 18 14:10:31 2000 +0200
+++ b/Admin/page/main-content/index.content	Mon Sep 18 14:35:54 2000 +0200
@@ -36,37 +36,21 @@
 
 <h2>Obtaining Isabelle</h2>
 
-Visit the <a href="dist/">download page</a>.
+See the <a href="dist/">download page</a>.
 <p>
-  Several mirror sites provide the Isabelle <a
-  href="dist/">distribution</a>, which includes <a
-  href="dist/source.html">sources</a>, <a
-  href="dist/binary.html">binary packages</a>, and <a
-  href="dist/docs.html">documentation</a>. 
-  The current version is <strong><!-- _GP_ distname --></strong>.
+
+Several mirror sites provide the Isabelle <a
+href="dist/">distribution</a>, which includes source and binary <a
+href="dist/packages.html">packages</a> and browsable <a
+href="dist/docs.html">documentation</a>.  The current version is
+<strong><!-- _GP_ distname --></strong>.
 
 <p>
 
-You can also browse the main Isabelle logics
-<a href="library/HOL/">HOL</a>, <a href="library/HOLCF/">HOLCF</a>, 
-<a href="library/FOL/">FOL</a> and <a href="library/ZF/">ZF</a> online.
-
-<p>
-&nbsp;
-
-<h2>User interface</h2>
-
-The distribution includes only a very primitive interface based on
-ordinary terminal sessions.
-
-<p>
-
-<a href="http://zermelo.dcs.ed.ac.uk/~proofgen/">Proof General</a> is
-a generic Emacs interface for proof assistants, including Isabelle
-(both for the classic and Isar version).  Proof General is suitable
-for use by pacifists and Emacs militants alike. Its most prominent
-feature is script management, providing a metaphor of <em>live proof
-script editing</em>.
+You can also browse the Isabelle theory <a href="library">library</a>;
+the main logics are <a href="library/HOL/">HOL</a>, <a
+href="library/HOLCF/">HOLCF</a>, <a href="library/FOL/">FOL</a> and <a
+href="library/ZF/">ZF</a>.
 
 <p>
 &nbsp;
@@ -75,5 +59,5 @@
 
 Use the mailing list <a href="mailto:
 isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> to
-discuss problems and results.  
-(Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?)
+discuss problems and results.  Why not <A
+HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?
diff -r 8c16ec5ba62b -r 3833b58a5d88 Admin/page/main-layout/template.html
--- a/Admin/page/main-layout/template.html	Mon Sep 18 14:10:31 2000 +0200
+++ b/Admin/page/main-layout/template.html	Mon Sep 18 14:35:54 2000 +0200
@@ -15,7 +15,7 @@
 
   <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
 
-    <table border="0" cellspacing="5" width="100%" height="100%">
+    <table border="0" cellspacing="5" width="100%">
 
       <tr>
         <td width="20%" valign="top" bgcolor="#aacccc">