1.1 --- a/doc-src/ZF/IFOL_examples.thy	Thu Jul 26 12:27:47 2012 +0200
     1.2 +++ b/doc-src/ZF/IFOL_examples.thy	Thu Jul 26 12:32:25 2012 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  header{*Examples of Intuitionistic Reasoning*}
     1.5  
     1.6 -theory IFOL_examples imports IFOL begin
     1.7 +theory IFOL_examples imports "~~/src/FOL/IFOL" begin
     1.8  
     1.9  text{*Quantifier example from the book Logic and Computation*}
    1.10  lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"