src/FOL/ROOT
author wenzelm
Sat, 22 Oct 2016 20:09:30 +0200
changeset 64349 26bc905be09d
parent 61935 6512e84cc9f5
child 65374 a5b38d8d3c1e
permissions -rw-r--r--
expose results on failure (via mail);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
51397
03b586ee5930 support for 'chapter' specifications within session ROOT;
wenzelm
parents: 48738
diff changeset
     1
chapter FOL
03b586ee5930 support for 'chapter' specifications within session ROOT;
wenzelm
parents: 48738
diff changeset
     2
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
     3
session FOL = Pure +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     4
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     5
    First-Order Logic with Natural Deduction (constructive and classical
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     6
    versions). For a classical sequent calculus, see Isabelle/LK.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     7
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     8
    Useful references on First-Order Logic:
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
     9
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    10
    Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    11
    1991) (The first chapter is an excellent introduction to natural deduction
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    12
    in general.)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    13
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    14
    Antony Galton, Logic for Information Technology (Wiley, 1990)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    15
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    16
    Michael Dummett, Elements of Intuitionism (Oxford, 1977)
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    17
  *}
56801
8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents: 56781
diff changeset
    18
  global_theories
8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents: 56781
diff changeset
    19
    IFOL
8dd9df88f647 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents: 56781
diff changeset
    20
    FOL
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 52488
diff changeset
    21
  document_files "root.tex"
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    22
48738
f8c1a5b9488f simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents: 48487
diff changeset
    23
session "FOL-ex" in ex = FOL +
51403
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    24
  description {*
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    25
    Examples for First-Order Logic.
2ff3a5589b05 refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents: 51397
diff changeset
    26
  *}
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    27
  theories
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    28
    Natural_Numbers
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    29
    Intro
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    30
    Nat
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    31
    Nat_Class
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    32
    Foundation
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    33
    Prolog
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    34
    Intuitionistic
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    35
    Propositional_Int
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    36
    Quantifiers_Int
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    37
    Classical
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    38
    Propositional_Cla
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    39
    Quantifiers_Cla
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    40
    Miniscope
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    41
    If
51558
91f8bed6d0a4 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents: 51403
diff changeset
    42
  theories [document = false, skip_proofs = false]
91f8bed6d0a4 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents: 51403
diff changeset
    43
    "Locale_Test/Locale_Test"
56781
f2eb0f22589f systematic replacement of 'files' by 'document_files';
wenzelm
parents: 52488
diff changeset
    44
  document_files "root.tex"
48280
7d86239986c2 basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff changeset
    45