equal
deleted
inserted
replaced
8 |
8 |
9 text {* |
9 text {* |
10 The following theory development demonstrates Higher-Order Logic |
10 The following theory development demonstrates Higher-Order Logic |
11 itself, represented directly within the Pure framework of Isabelle. |
11 itself, represented directly within the Pure framework of Isabelle. |
12 The ``HOL'' logic given here is essentially that of Gordon |
12 The ``HOL'' logic given here is essentially that of Gordon |
13 \cite{Gordon:1985:HOL}, although we prefer to present basic concepts |
13 @{cite "Gordon:1985:HOL"}, although we prefer to present basic concepts |
14 in a slightly more conventional manner oriented towards plain |
14 in a slightly more conventional manner oriented towards plain |
15 Natural Deduction. |
15 Natural Deduction. |
16 *} |
16 *} |
17 |
17 |
18 |
18 |