equal
deleted
inserted
replaced
1 chapter FOL |
1 chapter FOL |
2 |
2 |
3 session FOL = Pure + |
3 session FOL = Pure + |
4 description \<open> |
4 description " |
5 First-Order Logic with Natural Deduction (constructive and classical |
5 First-Order Logic with Natural Deduction (constructive and classical |
6 versions). For a classical sequent calculus, see Isabelle/LK. |
6 versions). For a classical sequent calculus, see Isabelle/LK. |
7 |
7 |
8 Useful references on First-Order Logic: |
8 Useful references on First-Order Logic: |
9 |
9 |
12 in general.) |
12 in general.) |
13 |
13 |
14 Antony Galton, Logic for Information Technology (Wiley, 1990) |
14 Antony Galton, Logic for Information Technology (Wiley, 1990) |
15 |
15 |
16 Michael Dummett, Elements of Intuitionism (Oxford, 1977) |
16 Michael Dummett, Elements of Intuitionism (Oxford, 1977) |
17 \<close> |
17 " |
18 theories |
18 theories |
19 IFOL (global) |
19 IFOL (global) |
20 FOL (global) |
20 FOL (global) |
21 document_files "root.tex" |
21 document_files "root.tex" |
22 |
22 |
23 session "FOL-ex" in ex = FOL + |
23 session "FOL-ex" in ex = FOL + |
24 description \<open> |
24 description " |
25 Examples for First-Order Logic. |
25 Examples for First-Order Logic. |
26 \<close> |
26 " |
27 theories |
27 theories |
28 Natural_Numbers |
28 Natural_Numbers |
29 Intro |
29 Intro |
30 Nat |
30 Nat |
31 Nat_Class |
31 Nat_Class |