tuned;

--- a/Admin/page/main-content/index.content	Mon Sep 18 14:49:58 2000 +0200
+++ b/Admin/page/main-content/index.content	Mon Sep 18 15:21:01 2000 +0200
@@ -5,9 +5,8 @@
 
 <p>
 
-<h2>Isabelle</h2> 
-is a popular generic theorem proving
-environment developed at Cambridge University (<a
+Isabelle is a popular generic theorem proving environment developed at
+Cambridge University (<a
 href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
 Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
 
@@ -31,29 +30,24 @@
 archives, research papers, the Isabelle bibliography, and Isabelle
 workshops and courses.
 
-<p>
-&nbsp;
 
 <h2>Obtaining Isabelle</h2>
 
-See the <a href="dist/">download page</a>.
-<p>
-
 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/index.html">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 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>.
+You can also browse the <a href="library/index.html">Isabelle theory
+library</a>; the main logics are <a
+href="library/HOL/index.html">HOL</a>, <a
+href="library/HOLCF/index.html">HOLCF</a>, <a
+href="library/FOL/index.html">FOL</a> and <a
+href="library/ZF/index.html">ZF</a>.
 
-<p>
-&nbsp;
 
 <h2>Mailing list</h2>
 

--- a/Admin/page/main-content/logics.content	Mon Sep 18 14:49:58 2000 +0200
+++ b/Admin/page/main-content/logics.content	Mon Sep 18 15:21:01 2000 +0200
@@ -2,7 +2,6 @@
 Isabelle's Logics
 
 %body%
-<h3>What is Isabelle?</h3>
 
 Isabelle can be viewed from two main perspectives.  On the one hand it
 may serve as a generic framework for rapid prototyping of deductive
@@ -19,20 +18,24 @@
 
 <dl>
 
-<dt><a href="library/HOL/"><strong>Isabelle/HOL</strong></a><dd> is a
-version of classical higher-order logic resembling that of the <A
+<dt><a
+href="library/HOL/index.html"><strong>Isabelle/HOL</strong></a><dd> is
+a version of classical higher-order logic resembling that of the <A
 HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL
 System</A>.
 
-<dt><a href="library/HOLCF/"><strong>Isabelle/HOLCF</strong></a><dd>
+<dt><a
+href="library/HOLCF/index.html"><strong>Isabelle/HOLCF</strong></a><dd>
 adds Scott's Logic for Computable Functions (domain theory) to HOL.
 
-<dt><a href="library/FOL/"><strong>Isabelle/FOL</strong></a><dd>
+<dt><a
+href="library/FOL/index.html"><strong>Isabelle/FOL</strong></a><dd>
 provides basic classical and intuitionistic first-order logic.  It is
 polymorphic.
 
-<dt><a href="library/ZF/"><strong>Isabelle/ZF</strong></a><dd> offers
-a formulation of Zermelo-Fraenkel set theory on top of FOL.
+<dt><a
+href="library/ZF/index.html"><strong>Isabelle/ZF</strong></a><dd>
+offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
 
 </dl>
 
@@ -43,8 +46,9 @@
 for advanced definitional concepts (like (co-)inductive sets and
 types, well-founded recursion etc.).  The distribution also includes
 some large applications, for example correctness proofs of
-cryptographic protocols (<a href="library/HOL/Auth/">HOL/Auth</a>) or
-communication protocols (<a href="library/HOLCF/IOA/">HOLCF/IOA</a>).
+cryptographic protocols (<a
+href="library/HOL/Auth/index.html">HOL/Auth</a>) or communication
+protocols (<a href="library/HOLCF/IOA/index.html">HOLCF/IOA</a>).
 
 <p>
 
@@ -56,11 +60,12 @@
 <p>
 
 There are a few minor object logics that may serve as further
-examples: <a href="library/CTT/">CTT</a> is an extensional version of
-Martin-L&ouml;f's Type Theory, <a href="library/Cube/">Cube</a> is
-Barendregt's Lambda Cube.  There are also some sequent calculus
-examples under <a href="library/Sequents/">Sequents</a>, including
-modal and linear logics.  Again see the <a href="library/">Isabelle
+examples: <a href="library/CTT/index.html">CTT</a> is an extensional
+version of Martin-L&ouml;f's Type Theory, <a
+href="library/Cube/index.html">Cube</a> is Barendregt's Lambda Cube.
+There are also some sequent calculus examples under <a
+href="library/Sequents/index.html">Sequents</a>, including modal and
+linear logics.  Again see the <a href="library/index.html">Isabelle
 theory library</a> for other examples.
 
 

--- a/Admin/page/main-content/munich.content	Mon Sep 18 14:49:58 2000 +0200
+++ b/Admin/page/main-content/munich.content	Mon Sep 18 15:21:01 2000 +0200
@@ -14,6 +14,7 @@
 Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
 This is the local page of the Munich group.
 
+
 <h2>People</h2>
 
 The following people are involved in Isabelle applications or