equal
deleted
inserted
replaced
3 Author: Gertrud Bauer and Markus Wenzel, TU Muenchen |
3 Author: Gertrud Bauer and Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Foundations of HOL *} |
6 header {* Foundations of HOL *} |
7 |
7 |
8 theory Higher_Order_Logic = CPure: |
8 theory Higher_Order_Logic imports CPure begin |
9 |
9 |
10 text {* |
10 text {* |
11 The following theory development demonstrates Higher-Order Logic |
11 The following theory development demonstrates Higher-Order Logic |
12 itself, represented directly within the Pure framework of Isabelle. |
12 itself, represented directly within the Pure framework of Isabelle. |
13 The ``HOL'' logic given here is essentially that of Gordon |
13 The ``HOL'' logic given here is essentially that of Gordon |