--- 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."
--- 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ö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>
--- 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 "
--- 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 "
--- 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 "
--- 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 "
--- 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 "
--- 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 "
--- 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