# HG changeset patch
# User wenzelm
# Date 1343298745 -7200
# Node ID 8f3069015441db73efc0faac2fc3ee154dbcaf00
# Parent  4854ced3e9d77a2b54db5e1a2c4a49b3cc911537
proper imports;

diff -r 4854ced3e9d7 -r 8f3069015441 doc-src/ZF/IFOL_examples.thy
--- 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))"