equal
deleted
inserted
replaced
4 |
4 |
5 Isabelle/HOL is a version of classical higher-order logic resembling |
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). |
6 that of the HOL System (https://www.cl.cam.ac.uk/Research/HVG/HOL). |
7 " |
7 " |
8 |
8 |
9 chapter_definition ZF |
|
10 description " |
|
11 Zermelo-Fraenkel set theory. |
|
12 |
|
13 Isabelle/ZF offers a formulation of Zermelo-Fraenkel set theory on top of |
|
14 Isabelle/FOL. |
|
15 " |
|
16 |
|
17 chapter_definition FOL |
9 chapter_definition FOL |
18 description " |
10 description " |
19 First-Order Logic with some variations: single-sorted vs. many-sorted |
11 First-Order Logic with some variations: single-sorted vs. many-sorted |
20 (polymorphic), classical vs. intuitionistic, domain-theory (LCF). |
12 (polymorphic), classical vs. intuitionistic, domain-theory (LCF) vs. |
|
13 set-theory (ZF). |
21 " |
14 " |
22 |
15 |
23 chapter_definition Pure |
16 chapter_definition Pure |
24 description " |
17 description " |
25 The Pure logical framework. |
18 The Pure logical framework. |