diff -r b05cd411d3d3 -r 2ff3a5589b05 src/FOL/ROOT
--- 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