1.1 --- a/Admin/page/main-content/index.content	Mon Sep 18 14:49:58 2000 +0200
     1.2 +++ b/Admin/page/main-content/index.content	Mon Sep 18 15:21:01 2000 +0200
     1.3 @@ -5,9 +5,8 @@
     1.4  
     1.5  <p>
     1.6  
     1.7 -<h2>Isabelle</h2> 
     1.8 -is a popular generic theorem proving
     1.9 -environment developed at Cambridge University (<a
    1.10 +Isabelle is a popular generic theorem proving environment developed at
    1.11 +Cambridge University (<a
    1.12  href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
    1.13  Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
    1.14  
    1.15 @@ -31,29 +30,24 @@
    1.16  archives, research papers, the Isabelle bibliography, and Isabelle
    1.17  workshops and courses.
    1.18  
    1.19 -<p>
    1.20 -&nbsp;
    1.21  
    1.22  <h2>Obtaining Isabelle</h2>
    1.23  
    1.24 -See the <a href="dist/">download page</a>.
    1.25 -<p>
    1.26 -
    1.27  Several mirror sites provide the Isabelle <a
    1.28 -href="dist/">distribution</a>, which includes source and binary <a
    1.29 -href="dist/packages.html">packages</a> and browsable <a
    1.30 +href="dist/index.html">distribution</a>, which includes source and
    1.31 +binary <a href="dist/packages.html">packages</a> and browsable <a
    1.32  href="dist/docs.html">documentation</a>.  The current version is
    1.33  <strong><!-- _GP_ distname --></strong>.
    1.34  
    1.35  <p>
    1.36  
    1.37 -You can also browse the Isabelle theory <a href="library">library</a>;
    1.38 -the main logics are <a href="library/HOL/">HOL</a>, <a
    1.39 -href="library/HOLCF/">HOLCF</a>, <a href="library/FOL/">FOL</a> and <a
    1.40 -href="library/ZF/">ZF</a>.
    1.41 +You can also browse the <a href="library/index.html">Isabelle theory
    1.42 +library</a>; the main logics are <a
    1.43 +href="library/HOL/index.html">HOL</a>, <a
    1.44 +href="library/HOLCF/index.html">HOLCF</a>, <a
    1.45 +href="library/FOL/index.html">FOL</a> and <a
    1.46 +href="library/ZF/index.html">ZF</a>.
    1.47  
    1.48 -<p>
    1.49 -&nbsp;
    1.50  
    1.51  <h2>Mailing list</h2>
    1.52  

     2.1 --- a/Admin/page/main-content/logics.content	Mon Sep 18 14:49:58 2000 +0200
     2.2 +++ b/Admin/page/main-content/logics.content	Mon Sep 18 15:21:01 2000 +0200
     2.3 @@ -2,7 +2,6 @@
     2.4  Isabelle's Logics
     2.5  
     2.6  %body%
     2.7 -<h3>What is Isabelle?</h3>
     2.8  
     2.9  Isabelle can be viewed from two main perspectives.  On the one hand it
    2.10  may serve as a generic framework for rapid prototyping of deductive
    2.11 @@ -19,20 +18,24 @@
    2.12  
    2.13  <dl>
    2.14  
    2.15 -<dt><a href="library/HOL/"><strong>Isabelle/HOL</strong></a><dd> is a
    2.16 -version of classical higher-order logic resembling that of the <A
    2.17 +<dt><a
    2.18 +href="library/HOL/index.html"><strong>Isabelle/HOL</strong></a><dd> is
    2.19 +a version of classical higher-order logic resembling that of the <A
    2.20  HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL
    2.21  System</A>.
    2.22  
    2.23 -<dt><a href="library/HOLCF/"><strong>Isabelle/HOLCF</strong></a><dd>
    2.24 +<dt><a
    2.25 +href="library/HOLCF/index.html"><strong>Isabelle/HOLCF</strong></a><dd>
    2.26  adds Scott's Logic for Computable Functions (domain theory) to HOL.
    2.27  
    2.28 -<dt><a href="library/FOL/"><strong>Isabelle/FOL</strong></a><dd>
    2.29 +<dt><a
    2.30 +href="library/FOL/index.html"><strong>Isabelle/FOL</strong></a><dd>
    2.31  provides basic classical and intuitionistic first-order logic.  It is
    2.32  polymorphic.
    2.33  
    2.34 -<dt><a href="library/ZF/"><strong>Isabelle/ZF</strong></a><dd> offers
    2.35 -a formulation of Zermelo-Fraenkel set theory on top of FOL.
    2.36 +<dt><a
    2.37 +href="library/ZF/index.html"><strong>Isabelle/ZF</strong></a><dd>
    2.38 +offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
    2.39  
    2.40  </dl>
    2.41  
    2.42 @@ -43,8 +46,9 @@
    2.43  for advanced definitional concepts (like (co-)inductive sets and
    2.44  types, well-founded recursion etc.).  The distribution also includes
    2.45  some large applications, for example correctness proofs of
    2.46 -cryptographic protocols (<a href="library/HOL/Auth/">HOL/Auth</a>) or
    2.47 -communication protocols (<a href="library/HOLCF/IOA/">HOLCF/IOA</a>).
    2.48 +cryptographic protocols (<a
    2.49 +href="library/HOL/Auth/index.html">HOL/Auth</a>) or communication
    2.50 +protocols (<a href="library/HOLCF/IOA/index.html">HOLCF/IOA</a>).
    2.51  
    2.52  <p>
    2.53  
    2.54 @@ -56,11 +60,12 @@
    2.55  <p>
    2.56  
    2.57  There are a few minor object logics that may serve as further
    2.58 -examples: <a href="library/CTT/">CTT</a> is an extensional version of
    2.59 -Martin-L&ouml;f's Type Theory, <a href="library/Cube/">Cube</a> is
    2.60 -Barendregt's Lambda Cube.  There are also some sequent calculus
    2.61 -examples under <a href="library/Sequents/">Sequents</a>, including
    2.62 -modal and linear logics.  Again see the <a href="library/">Isabelle
    2.63 +examples: <a href="library/CTT/index.html">CTT</a> is an extensional
    2.64 +version of Martin-L&ouml;f's Type Theory, <a
    2.65 +href="library/Cube/index.html">Cube</a> is Barendregt's Lambda Cube.
    2.66 +There are also some sequent calculus examples under <a
    2.67 +href="library/Sequents/index.html">Sequents</a>, including modal and
    2.68 +linear logics.  Again see the <a href="library/index.html">Isabelle
    2.69  theory library</a> for other examples.
    2.70  
    2.71  

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