1chapter FOL
2
3session FOL = Pure +
4  description "
5    First-Order Logic with Natural Deduction (constructive and classical
6    versions). For a classical sequent calculus, see Isabelle/LK.
7
8    Useful references on First-Order Logic:
9
10    Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
11    1991) (The first chapter is an excellent introduction to natural deduction
12    in general.)
13
14    Antony Galton, Logic for Information Technology (Wiley, 1990)
15
16    Michael Dummett, Elements of Intuitionism (Oxford, 1977)
17  "
18  theories
19    IFOL (global)
20    FOL (global)
21  document_files "root.tex"
22
23session "FOL-ex" in ex = FOL +
24  description "
25    Examples for First-Order Logic.
26  "
27  directories "Locale_Test"
28  theories
29    Natural_Numbers
30    Intro
31    Nat
32    Nat_Class
33    Foundation
34    Prolog
35    Intuitionistic
36    Propositional_Int
37    Quantifiers_Int
38    Classical
39    Propositional_Cla
40    Quantifiers_Cla
41    Miniscope
42    If
43  theories [document = false, skip_proofs = false]
44    "Locale_Test/Locale_Test"
45  document_files "root.tex"
46