# HG changeset patch
# User wenzelm
# Date 1661548362 -7200
# Node ID 1f6d79b6222296093b705ed7500b1d954d72bc70
# Parent  0dbf2b2c04f40a580b7099e70e90b1241438cee3
clarified chapters: de-emphasize minor examples;

diff -r 0dbf2b2c04f4 -r 1f6d79b62222 ROOT
--- a/ROOT	Fri Aug 26 21:55:03 2022 +0200
+++ b/ROOT	Fri Aug 26 23:12:42 2022 +0200
@@ -6,40 +6,20 @@
     that of the HOL System (https://www.cl.cam.ac.uk/Research/HVG/HOL).
   "
 
-chapter_definition FOL
-  description "
-    Many-sorted First-Order Logic.
-
-    Isabelle/FOL provides basic classical and intuitionistic first-order logic.
-    It is polymorphic.
-  "
-
 chapter_definition ZF
   description "
-    Isabelle/ZF (Set Theory) offers a formulation of Zermelo-Fraenkel set theory
-    on top of Isabelle/FOL.
+    Zermelo-Fraenkel set theory.
+
+    Isabelle/ZF offers a formulation of Zermelo-Fraenkel set theory on top of
+    Isabelle/FOL.
   "
 
-chapter_definition CCL
-  description "Classical Computational Logic."
-
-chapter_definition LCF
-  description "Logic of Computable Functions."
-
-chapter_definition FOLP
-  description "FOL with Proof Terms."
-
-chapter_definition Sequents
-  description "First-order, modal and linear logics."
-
-chapter_definition CTT
+chapter_definition FOL
   description "
-    Constructive Type Theory: an extensional version of Martin-Löf's Type Theory.
+    First-Order Logic with some variations: single-sorted vs. many-sorted
+    (polymorphic), classical vs. intuitionistic, domain-theory (LCF).
   "
 
-chapter_definition Cube
-  description "Barendregt's Lambda Cube."
-
 chapter_definition Pure
   description "
     The Pure logical framework.
@@ -48,8 +28,8 @@
     expresses rules for Natural Deduction declaratively.
   "
 
+chapter_definition Misc
+  description "Miscellaneous object-logics, tools, and experiments."
+
 chapter_definition Doc
   description "Sources of Documentation."
-
-chapter_definition Tools
-  description "Miscellaneous tools."
diff -r 0dbf2b2c04f4 -r 1f6d79b62222 lib/html/library_index_content.template
--- a/lib/html/library_index_content.template	Fri Aug 26 21:55:03 2022 +0200
+++ b/lib/html/library_index_content.template	Fri Aug 26 23:12:42 2022 +0200
@@ -16,20 +16,20 @@
 
     <li style="list-style: none">
       <ul>
-        <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
+        <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="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="ZF/index.html">ZF (Set Theory)</a>
-        offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
-        </li>
+        <li><a href="FOL/CCL/index.html">CCL (Classical Computational Logic)</a></li>
 
-        <li><a href="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="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="FOL/FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
       </ul>
     </li>
   </ul>
@@ -39,12 +39,12 @@
 
     <li style="list-style: none">
       <ul>
-        <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
+        <li><a href="Misc/Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
 
-        <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
+        <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="Cube/index.html">Cube (The Lambda Cube)</a></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>
 
diff -r 0dbf2b2c04f4 -r 1f6d79b62222 src/CCL/ROOT
--- a/src/CCL/ROOT	Fri Aug 26 21:55:03 2022 +0200
+++ b/src/CCL/ROOT	Fri Aug 26 23:12:42 2022 +0200
@@ -1,4 +1,4 @@
-chapter CCL
+chapter FOL
 
 session CCL = Pure +
   description "
diff -r 0dbf2b2c04f4 -r 1f6d79b62222 src/CTT/ROOT
--- a/src/CTT/ROOT	Fri Aug 26 21:55:03 2022 +0200
+++ b/src/CTT/ROOT	Fri Aug 26 23:12:42 2022 +0200
@@ -1,4 +1,4 @@
-chapter CTT
+chapter Misc
 
 session CTT = Pure +
   description "
diff -r 0dbf2b2c04f4 -r 1f6d79b62222 src/Cube/ROOT
--- a/src/Cube/ROOT	Fri Aug 26 21:55:03 2022 +0200
+++ b/src/Cube/ROOT	Fri Aug 26 23:12:42 2022 +0200
@@ -1,4 +1,4 @@
-chapter Cube
+chapter Misc
 
 session Cube = Pure +
   description "
diff -r 0dbf2b2c04f4 -r 1f6d79b62222 src/FOLP/ROOT
--- a/src/FOLP/ROOT	Fri Aug 26 21:55:03 2022 +0200
+++ b/src/FOLP/ROOT	Fri Aug 26 23:12:42 2022 +0200
@@ -1,4 +1,4 @@
-chapter FOLP
+chapter FOL
 
 session FOLP = Pure +
   description "
diff -r 0dbf2b2c04f4 -r 1f6d79b62222 src/LCF/ROOT
--- a/src/LCF/ROOT	Fri Aug 26 21:55:03 2022 +0200
+++ b/src/LCF/ROOT	Fri Aug 26 23:12:42 2022 +0200
@@ -1,4 +1,4 @@
-chapter LCF
+chapter FOL
 
 session LCF = Pure +
   description "
diff -r 0dbf2b2c04f4 -r 1f6d79b62222 src/Sequents/ROOT
--- a/src/Sequents/ROOT	Fri Aug 26 21:55:03 2022 +0200
+++ b/src/Sequents/ROOT	Fri Aug 26 23:12:42 2022 +0200
@@ -1,4 +1,4 @@
-chapter Sequents
+chapter Misc
 
 session Sequents = Pure +
   description "
diff -r 0dbf2b2c04f4 -r 1f6d79b62222 src/Tools/ROOT
--- a/src/Tools/ROOT	Fri Aug 26 21:55:03 2022 +0200
+++ b/src/Tools/ROOT	Fri Aug 26 23:12:42 2022 +0200
@@ -1,4 +1,4 @@
-chapter Tools
+chapter Misc
 
 session Tools = Pure +
   theories