equal
deleted
inserted
replaced
1 (* Title: FOL/ex/First_Order_Logic.thy |
1 (* Title: FOL/ex/First_Order_Logic.thy |
2 Author: Markus Wenzel, TU Munich |
2 Author: Markus Wenzel, TU Munich |
3 *) |
3 *) |
4 |
4 |
5 header {* A simple formulation of First-Order Logic *} |
5 section {* A simple formulation of First-Order Logic *} |
6 |
6 |
7 theory First_Order_Logic imports Pure begin |
7 theory First_Order_Logic imports Pure begin |
8 |
8 |
9 text {* |
9 text {* |
10 The subsequent theory development illustrates single-sorted |
10 The subsequent theory development illustrates single-sorted |