1.1 --- a/doc-src/ZF/FOL_examples.thy	Thu Jul 26 14:29:54 2012 +0200
     1.2 +++ b/doc-src/ZF/FOL_examples.thy	Thu Jul 26 14:44:07 2012 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  header{*Examples of Classical Reasoning*}
     1.5  
     1.6 -theory FOL_examples imports FOL begin
     1.7 +theory FOL_examples imports "~~/src/FOL/FOL" begin
     1.8  
     1.9  lemma "EX y. ALL x. P(y)-->P(x)"
    1.10    --{* @{subgoals[display,indent=0,margin=65]} *}

     2.1 --- a/doc-src/ZF/If.thy	Thu Jul 26 14:29:54 2012 +0200
     2.2 +++ b/doc-src/ZF/If.thy	Thu Jul 26 14:44:07 2012 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  First-Order Logic: the 'if' example.
     2.5  *)
     2.6  
     2.7 -theory If imports FOL begin
     2.8 +theory If imports "~~/src/FOL/FOL" begin
     2.9  
    2.10  definition "if" :: "[o,o,o]=>o" where
    2.11    "if(P,Q,R) == P&Q | ~P&R"