proper imports;

--- a/doc-src/ZF/IFOL_examples.thy	Thu Jul 26 12:27:47 2012 +0200
+++ b/doc-src/ZF/IFOL_examples.thy	Thu Jul 26 12:32:25 2012 +0200
@@ -1,6 +1,6 @@
 header{*Examples of Intuitionistic Reasoning*}
 
-theory IFOL_examples imports IFOL begin
+theory IFOL_examples imports "~~/src/FOL/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))"