# HG changeset patch # User wenzelm # Date 1635937462 -3600 # Node ID b2604cd4d131234a83974a04b05948389fd2bb2f # Parent 0b3dc8c5fb326a5ffe8569aa2468e00ab9e5c0a4 recover library_index_content.template from c337c798f64c: required for website/build/main; diff -r 0b3dc8c5fb32 -r b2604cd4d131 lib/html/library_index_content.template --- /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 @@ +

Higher-Order Logic
+
- HOL (Higher-Order Logic) + is a version of classical higher-order logic resembling + that of the HOL System. +
+

+ +

First-Order Logic
+
- FOL (Many-sorted First-Order Logic) + provides basic classical and intuitionistic first-order logic. It is + polymorphic. +
- ZF (Set Theory) + offers a formulation of Zermelo-Fraenkel set theory on top of FOL. +
- CCL (Classical Computational Logic)
- LCF (Logic of Computable Functions)
- FOLP (FOL with Proof Terms)
+

+ +

Miscellaneous
+
- Sequents (first-order, modal and linear logics)
- CTT (Constructive Type Theory) + is an extensional version of Martin-Löf's Type Theory.
- Cube (The Lambda Cube)
- The Pure logical framework
- Sources of Documentation
+

diff -r 0b3dc8c5fb32 -r b2604cd4d131 src/Pure/Thy/presentation.scala --- 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 @@

Higher-Order Logic
-
- HOL (Higher-Order Logic) - is a version of classical higher-order logic resembling - that of the HOL System. -
-

- -

First-Order Logic
-
- FOL (Many-sorted First-Order Logic) - provides basic classical and intuitionistic first-order logic. It is - polymorphic. -
- ZF (Set Theory) - offers a formulation of Zermelo-Fraenkel set theory on top of FOL. -
- CCL (Classical Computational Logic)
- LCF (Logic of Computable Functions)
- FOLP (FOL with Proof Terms)
-

- -

Miscellaneous
-
- Sequents (first-order, modal and linear logics)
- CTT (Constructive Type Theory) - is an extensional version of Martin-Löf's Type Theory.
- Cube (The Lambda Cube)
- The Pure logical framework
- Sources of Documentation
-

+""" + File.read(Path.explode("~~/lib/html/library_index_content.template")) + +""" """ + HTML.footer) }