doc-src/ZF/FOL_examples.thy

 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]} *}
 apply (rule exCI)
   --{* @{subgoals[display,indent=0,margin=65]} *}