src/FOL/ROOT
author haftmann
Thu Nov 23 17:03:27 2017 +0000 (20 months ago)
changeset 67087 733017b19de9
parent 65374 a5b38d8d3c1e
child 69272 15e9ed5b28fb
permissions -rw-r--r--
generalized more lemmas
     1 chapter FOL
     2 
     3 session 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 
    23 session "FOL-ex" in ex = FOL +
    24   description {*
    25     Examples for First-Order Logic.
    26   *}
    27   theories
    28     Natural_Numbers
    29     Intro
    30     Nat
    31     Nat_Class
    32     Foundation
    33     Prolog
    34     Intuitionistic
    35     Propositional_Int
    36     Quantifiers_Int
    37     Classical
    38     Propositional_Cla
    39     Quantifiers_Cla
    40     Miniscope
    41     If
    42   theories [document = false, skip_proofs = false]
    43     "Locale_Test/Locale_Test"
    44   document_files "root.tex"
    45