src/FOL/ROOT
author traytel
Mon, 24 Oct 2016 16:53:32 +0200
changeset 64379 71f42dcaa1df
parent 61935 6512e84cc9f5
child 65374 a5b38d8d3c1e
permissions -rw-r--r--
additional user-specified simp (naturality) rules used in friend_of_corec

chapter FOL

session FOL = Pure +
  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)
  *}
  global_theories
    IFOL
    FOL
  document_files "root.tex"

session "FOL-ex" in ex = FOL +
  description {*
    Examples for First-Order Logic.
  *}
  theories
    Natural_Numbers
    Intro
    Nat
    Nat_Class
    Foundation
    Prolog
    Intuitionistic
    Propositional_Int
    Quantifiers_Int
    Classical
    Propositional_Cla
    Quantifiers_Cla
    Miniscope
    If
  theories [document = false, skip_proofs = false]
    "Locale_Test/Locale_Test"
  document_files "root.tex"