| changeset 42637 | 381fdcab0f36 |
| parent 42628 | 50f257ea2aba |
| child 42673 | 43766deefc16 |
| 42636:41dff1b862bf | 42637:381fdcab0f36 |
|---|---|
1 %% $Id$ |
|
2 \chapter{Higher-Order Logic} |
1 \chapter{Higher-Order Logic} |
3 \index{higher-order logic|(} |
2 \index{higher-order logic|(} |
4 \index{HOL system@{\sc hol} system} |
3 \index{HOL system@{\sc hol} system} |
5 |
4 |
6 The theory~\thydx{HOL} implements higher-order logic. It is based on |
5 The theory~\thydx{HOL} implements higher-order logic. It is based on |