| changeset 58889 | 5b7a9633cfa8 |
| parent 58618 | 782f0b662cae |
| child 58999 | ed09ae4ea2d8 |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
1 |
1 |
2 header \<open>Example: First-Order Logic\<close> |
2 section \<open>Example: First-Order Logic\<close> |
3 |
3 |
4 theory %visible First_Order_Logic |
4 theory %visible First_Order_Logic |
5 imports Base (* FIXME Pure!? *) |
5 imports Base (* FIXME Pure!? *) |
6 begin |
6 begin |
7 |
7 |