| changeset 16417 | 9bc16273c2d4 |
| parent 14152 | 12f6f18e7afc |
| child 48517 | 0f8c8ac6cc0e |
--- a/doc-src/ZF/FOL_examples.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/doc-src/ZF/FOL_examples.thy Fri Jun 17 16:12:49 2005 +0200 @@ -1,6 +1,6 @@ header{*Examples of Classical Reasoning*} -theory FOL_examples = FOL: +theory FOL_examples imports FOL begin lemma "EX y. ALL x. P(y)-->P(x)" --{* @{subgoals[display,indent=0,margin=65]} *}