--- a/src/FOL/ROOT Tue Mar 12 20:03:04 2013 +0100
+++ b/src/FOL/ROOT Tue Mar 12 21:59:48 2013 +0100
@@ -1,12 +1,28 @@
chapter FOL
session FOL = Pure +
- description "First-Order Logic with Natural Deduction"
+ description {*
+ First-Order Logic with Natural Deduction (constructive and classical
+ versions). For a classical sequent calculus, see Isabelle/LK.
+
+ Useful references on First-Order Logic:
+
+ Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
+ 1991) (The first chapter is an excellent introduction to natural deduction
+ in general.)
+
+ Antony Galton, Logic for Information Technology (Wiley, 1990)
+
+ Michael Dummett, Elements of Intuitionism (Oxford, 1977)
+ *}
options [proofs = 2]
theories FOL
files "document/root.tex"
session "FOL-ex" in ex = FOL +
+ description {*
+ Examples for First-Order Logic.
+ *}
theories
First_Order_Logic
Natural_Numbers