| changeset 58889 | 5b7a9633cfa8 |
| parent 56451 | 856492b0f755 |
| child 66453 | cc19f7ca2ed6 |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
1 header{*Examples of Classical Reasoning*} |
1 section{*Examples of Classical Reasoning*} |
2 |
2 |
3 theory FOL_examples imports "~~/src/FOL/FOL" begin |
3 theory FOL_examples imports "~~/src/FOL/FOL" begin |
4 |
4 |
5 lemma "EX y. ALL x. P(y)-->P(x)" |
5 lemma "EX y. ALL x. P(y)-->P(x)" |
6 --{* @{subgoals[display,indent=0,margin=65]} *} |
6 --{* @{subgoals[display,indent=0,margin=65]} *} |