# HG changeset patch
# User wenzelm
# Date 1343306647 -7200
# Node ID 0f8c8ac6cc0eb19125ccd0d49111a8220a5f9315
# Parent  c5d0f19ef7cba7ffee2fd7e58425ffbdfef4d0d3
more precise imports;

diff -r c5d0f19ef7cb -r 0f8c8ac6cc0e doc-src/ZF/FOL_examples.thy
--- a/doc-src/ZF/FOL_examples.thy	Thu Jul 26 14:29:54 2012 +0200
+++ b/doc-src/ZF/FOL_examples.thy	Thu Jul 26 14:44:07 2012 +0200
@@ -1,6 +1,6 @@
 header{*Examples of Classical Reasoning*}
 
-theory FOL_examples imports FOL begin
+theory FOL_examples imports "~~/src/FOL/FOL" begin
 
 lemma "EX y. ALL x. P(y)-->P(x)"
   --{* @{subgoals[display,indent=0,margin=65]} *}
diff -r c5d0f19ef7cb -r 0f8c8ac6cc0e doc-src/ZF/If.thy
--- a/doc-src/ZF/If.thy	Thu Jul 26 14:29:54 2012 +0200
+++ b/doc-src/ZF/If.thy	Thu Jul 26 14:44:07 2012 +0200
@@ -5,7 +5,7 @@
 First-Order Logic: the 'if' example.
 *)
 
-theory If imports FOL begin
+theory If imports "~~/src/FOL/FOL" begin
 
 definition "if" :: "[o,o,o]=>o" where
   "if(P,Q,R) == P&Q | ~P&R"