--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/html/index.html	Fri May 05 22:24:03 2000 +0200
@@ -0,0 +1,60 @@
+<html>
+
+<head><title>The Isabelle Library ({ISABELLE})</title></head>
+
+<body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
+
+<center>
+  <table width="100%" border="0" cellspacing="10" cellpadding="0">
+    <tr>
+      <td width="20%" valign="middle" align="center">
+        <img align=bottom src="isabelle.gif" width="100" height="86" alt="[Isabelle]">
+      </td>
+      <td width="80%" valign="middle" align="center">
+        <table width="90%" border="0" cellspacing="0" cellpadding="20">
+          <tr>
+            <td valign="middle" align="center" bgcolor="#aacccc">
+              <font face="Helvetica,Arial" size="+2">The Isabelle Library</font>
+            </td>
+          </tr>
+        </table>
+      </td>
+    </tr>
+  </table>
+</center>
+
+<hr>
+
+Higher-Order Logic
+
+<ul>
+<li><a href="HOL/index.html"> HOL (Simply-typed Set Theory)</a>
+<li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a>
+</ul>
+
+<hr>
+
+First-Order Logic
+
+<ul>
+<li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
+<li><a href="ZF/index.html">ZF (Set Theory)</a>
+<li><a href="CCL/index.html">CCL (Classical Computational Logic)</a>
+<li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a>
+<li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a>
+</ul>
+
+<hr>
+
+Miscellaneous
+
+<ul>
+<li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a>
+<li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
+<li><a href="Cube/index.html">Cube (The Lambda Cube)</a>
+</ul>
+
+<hr>
+
+</body>
+</html>