lib/html/index.html
changeset 25233 9146551357f6
parent 25232 9b4d0c13c332
--- a/lib/html/index.html	Tue Oct 30 10:30:09 2007 +0100
+++ b/lib/html/index.html	Tue Oct 30 10:41:19 2007 +0100
@@ -8,19 +8,19 @@
   <meta name="generator" content="HTML Tidy for Linux/x86 (vers 31 October 2006), see www.w3.org" />
   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" />
 
-  <title>The Isabelle Library ({ISABELLE})</title>
+  <title>The {ISABELLE} Library</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="20%" valign="middle" align="center"><a href="http://isabelle.in.tum.de/"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" border="0" /></a></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>
+              <td valign="middle" align="center" bgcolor="#AACCCC"><font face="Helvetica,Arial" size="+2">The {ISABELLE} Library</font></td>
             </tr>
           </table>
         </td>
@@ -28,37 +28,49 @@
     </table>
   </center>
   <hr />
-  Higher-Order Logic
 
   <ul>
-    <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a></li>
+    <li>Higher-Order Logic</li>
 
-    <li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a></li>
+    <li style="list-style: none">
+      <ul>
+        <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a></li>
+
+        <li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a></li>
+      </ul>
+    </li>
   </ul>
-  <hr />
-  First-Order Logic
 
   <ul>
-    <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a></li>
+    <li>First-Order Logic</li>
 
-    <li><a href="ZF/index.html">ZF (Set Theory)</a></li>
+    <li style="list-style: none">
+      <ul>
+        <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a></li>
 
-    <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
+        <li><a href="ZF/index.html">ZF (Set Theory)</a></li>
 
-    <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
+        <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
+
+        <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
 
-    <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
+        <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
+      </ul>
+    </li>
   </ul>
-  <hr />
-  Miscellaneous
 
   <ul>
-    <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
+    <li>Miscellaneous</li>
 
-    <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a></li>
+    <li style="list-style: none">
+      <ul>
+        <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
 
-    <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
+        <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a></li>
+
+        <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
+      </ul>
+    </li>
   </ul>
-  <hr />
 </body>
 </html>