equal
deleted
inserted
replaced
1 header{*Examples of Intuitionistic Reasoning*} |
1 header{*Examples of Intuitionistic Reasoning*} |
2 |
2 |
3 theory IFOL_examples imports 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))" |
7 --{* @{subgoals[display,indent=0,margin=65]} *} |
7 --{* @{subgoals[display,indent=0,margin=65]} *} |
8 apply (rule impI) |
8 apply (rule impI) |