| changeset 58889 | 5b7a9633cfa8 |
| parent 56451 | 856492b0f755 |
| child 66453 | cc19f7ca2ed6 |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
1 header{*Examples of Intuitionistic Reasoning*} |
1 section{*Examples of Intuitionistic Reasoning*} |
2 |
2 |
3 theory IFOL_examples imports "~~/src/FOL/IFOL" begin |
3 theory IFOL_examples imports "~~/src/FOL/IFOL" begin |
4 |
4 |
5 text{*Quantifier example from the book Logic and Computation*} |
5 text{*Quantifier example from the book Logic and Computation*} |
6 lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" |
6 lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" |