| author | wenzelm |
| Tue, 24 Jul 2012 21:36:53 +0200 | |
| changeset 48487 | 94a9650f79fb |
| parent 48470 | 7483aa690b4f |
| child 48738 | f8c1a5b9488f |
| permissions | -rw-r--r-- |
| 48487 | 1 |
session FOL! in "." = Pure + |
|
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
2 |
description "First-Order Logic with Natural Deduction" |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
3 |
options [proofs = 2] |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
4 |
theories FOL |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
5 |
files "document/root.tex" |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
6 |
|
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
7 |
session ex = FOL + |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
8 |
theories |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
9 |
First_Order_Logic |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
10 |
Natural_Numbers |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
11 |
Intro |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
12 |
Nat |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
13 |
Nat_Class |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
14 |
Foundation |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
15 |
Prolog |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
16 |
Intuitionistic |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
17 |
Propositional_Int |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
18 |
Quantifiers_Int |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
19 |
Classical |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
20 |
Propositional_Cla |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
21 |
Quantifiers_Cla |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
22 |
Miniscope |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
23 |
If |
|
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset
|
24 |
theories [document = false] "Locale_Test/Locale_Test" |
|
48280
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
25 |
files "document/root.tex" |
|
7d86239986c2
basic support for session ROOT files, with examples for FOL and ZF;
wenzelm
parents:
diff
changeset
|
26 |