equal
deleted
inserted
replaced
|
1 chapter_definition HOL |
|
2 description " |
|
3 Higher-Order Logic. |
|
4 |
|
5 Isabelle/HOL is a version of classical higher-order logic resembling |
|
6 that of the HOL System (https://www.cl.cam.ac.uk/Research/HVG/HOL). |
|
7 " |
|
8 |
|
9 chapter_definition FOL |
|
10 description " |
|
11 First-Order Logic with some variations: single-sorted vs. many-sorted |
|
12 (polymorphic), classical vs. intuitionistic, domain-theory (LCF) vs. |
|
13 set-theory (ZF). |
|
14 " |
|
15 |
|
16 chapter_definition Pure |
|
17 description " |
|
18 The Pure logical framework. |
|
19 |
|
20 Isabelle/Pure is a version of intuitionistic higher-order logic that |
|
21 expresses rules for Natural Deduction declaratively. |
|
22 " |
|
23 |
|
24 chapter_definition Misc |
|
25 description " |
|
26 Miscellaneous object-logics, tools, and experiments. |
|
27 " |
|
28 |
|
29 chapter_definition Doc |
|
30 description " |
|
31 Sources of Documentation. |
|
32 " |
|
33 |
|
34 chapter_definition Unsorted |
|
35 description " |
|
36 Sessions without 'chapter' declaration. |
|
37 " |