Admin/website/logics.html

--- a/Admin/website/logics.html	Wed Sep 21 14:46:10 2005 +0200
+++ b/Admin/website/logics.html	Wed Sep 21 16:37:37 2005 +0200
@@ -24,25 +24,25 @@
       
       <p>The Isabelle distribution includes a large body of
       object logics and other examples (see the <a href=
-      "library/index.html">Isabelle theory library</a>).</p>
+      "//dist/library/index.html">Isabelle theory library</a>).</p>
     
       <dl>
-        <dt id="isabelle_hol"><a href="//library/HOL/index.html">Isabelle/HOL</a></dt>
+        <dt id="isabelle_hol"><a href="//dist/library/HOL/index.html">Isabelle/HOL</a></dt>
         <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 System</a>. The
         main libraries of the HOL 4 System are now <a href=
-        "library/HOL/HOL-Complex/HOL4/index.html">available in Isabelle</a>.</dd>
+        "//dist/library/HOL/HOL-Complex/HOL4/index.html">available in Isabelle</a>.</dd>
     
         <dt><a href=
-        "library/HOLCF/index.html">Isabelle/HOLCF</a></dt>
+        "//dist/library/HOLCF/index.html">Isabelle/HOLCF</a></dt>
         <dd>adds Scott's Logic for Computable Functions (domain theory) to
         HOL.</dd>
     
-        <dt><a href="//library/FOL/index.html">Isabelle/FOL</a></dt>
+        <dt><a href="//dist/library/FOL/index.html">Isabelle/FOL</a></dt>
         <dd>provides basic classical and intuitionistic first-order logic. It is
         polymorphic.</dd>
     
-        <dt><a href="//library/ZF/index.html">Isabelle/ZF</a></dt>
+        <dt><a href="//dist/library/ZF/index.html">Isabelle/ZF</a></dt>
             <dd>offers a formulation of Zermelo-Fraenkel set theory on top of FOL.</dd>
       </dl>
 
@@ -51,8 +51,8 @@
       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/index.html">HOL/Auth</a>) or communication
-      protocols (<a href="//library/HOLCF/IOA/index.html">HOLCF/IOA</a>).</p>
+      (<a href="//dist/library/HOL/Auth/index.html">HOL/Auth</a>) or communication
+      protocols (<a href="//dist/library/HOLCF/IOA/index.html">HOLCF/IOA</a>).</p>
     
       <p><em>Isabelle/ZF</em> provides another starting point for applications, with a
       slightly less developed library. Its definitional packages are similar to
@@ -60,11 +60,11 @@
       sets than simply-typed HOL.</p>
     
       <p>There are a few minor object logics that may serve as further 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
+      <a href="//dist/library/CTT/index.html">CTT</a> is an extensional version of
+      Martin-L&ouml;f's Type Theory, <a href="//dist/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
+      <a href="//dist/library/Sequents/index.html">Sequents</a>, including modal and
+      linear logics. Again see the <a href="//dist/library/index.html">Isabelle theory
       library</a> for other examples.</p>
     
       <h2>Defining Logics</h2>