diff --git a/lib/html/library_index_content.template b/lib/html/library_index_content.template
--- a/lib/html/library_index_content.template
+++ b/lib/html/library_index_content.template
@@ -1,54 +1,54 @@
   <ul>
     <li>Higher-Order Logic</li>
 
     <li style="list-style: none">
       <ul>
         <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
         is a version of classical higher-order logic resembling
         that of the <a href="https://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
         </li>
       </ul>
     </li>
   </ul>
 
   <ul>
     <li>First-Order Logic</li>
 
     <li style="list-style: none">
       <ul>
-        <li><a href="ZF/index.html">ZF (Set Theory)</a>
+        <li><a href="FOL/ZF/index.html">ZF (Set Theory)</a>
         offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
         </li>
 
         <li><a href="FOL/FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
         provides basic classical and intuitionistic first-order logic. It is
         polymorphic.
         </li>
 
         <li><a href="FOL/CCL/index.html">CCL (Classical Computational Logic)</a></li>
 
         <li><a href="FOL/LCF/index.html">LCF (Logic of Computable Functions)</a></li>
 
         <li><a href="FOL/FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
       </ul>
     </li>
   </ul>
 
   <ul>
     <li>Miscellaneous</li>
 
     <li style="list-style: none">
       <ul>
         <li><a href="Misc/Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
 
         <li><a href="Misc/CTT/index.html">CTT (Constructive Type Theory)</a>
         is an extensional version of Martin-L&ouml;f's Type Theory.</li>
 
         <li><a href="Misc/Cube/index.html">Cube (The Lambda Cube)</a></li>
 
         <li><a href="Pure/index.html">The Pure logical framework</a></li>
 
         <li><a href="Doc/index.html">Sources of Documentation</a></li>
       </ul>
     </li>
   </ul>