src/FOL/ROOT
author blanchet
Mon Sep 15 10:49:07 2014 +0200 (2014-09-15)
changeset 58335 a5a3b576fcfb
parent 56801 8dd9df88f647
child 61935 6512e84cc9f5
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
     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   global_theories
    19     IFOL
    20     FOL
    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     First_Order_Logic
    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