recover library_index_content.template from c337c798f64c: required for website/build/main;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/html/library_index_content.template	Wed Nov 03 12:04:22 2021 +0100
@@ -0,0 +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="http://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="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="ZF/index.html">ZF (Set Theory)</a>
+        offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
+        </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>
+      </ul>
+    </li>
+  </ul>
+
+  <ul>
+    <li>Miscellaneous</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="CTT/index.html">CTT (Constructive Type Theory)</a>
+        is an extensional version of Martin-L&ouml;f's Type Theory.</li>
+
+        <li><a href="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>

--- a/src/Pure/Thy/presentation.scala	Wed Nov 03 11:51:42 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Wed Nov 03 12:04:22 2021 +0100
@@ -279,60 +279,8 @@
     </table>
   </center>
   <hr />
-  <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="http://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="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="ZF/index.html">ZF (Set Theory)</a>
-        offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
-        </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>
-      </ul>
-    </li>
-  </ul>
-
-  <ul>
-    <li>Miscellaneous</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="CTT/index.html">CTT (Constructive Type Theory)</a>
-        is an extensional version of Martin-L&ouml;f's Type Theory.</li>
-
-        <li><a href="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>
+""" + File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+"""
 </body>
 """ + HTML.footer)
     }