| changeset 16417 | 9bc16273c2d4 |
| parent 14152 | 12f6f18e7afc |
| child 48510 | 8f3069015441 |
--- a/doc-src/ZF/IFOL_examples.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/doc-src/ZF/IFOL_examples.thy Fri Jun 17 16:12:49 2005 +0200 @@ -1,6 +1,6 @@ header{*Examples of Intuitionistic Reasoning*} -theory IFOL_examples = IFOL: +theory IFOL_examples imports IFOL begin text{*Quantifier example from the book Logic and Computation*} lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"