doc-src/ZF/If.thy
changeset 49532 0f8c8ac6cc0e
parent 43508 381fdcab0f36
     1.1 --- a/doc-src/ZF/If.thy	Thu Jul 26 14:29:54 2012 +0200
     1.2 +++ b/doc-src/ZF/If.thy	Thu Jul 26 14:44:07 2012 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  First-Order Logic: the 'if' example.
     1.5  *)
     1.6  
     1.7 -theory If imports FOL begin
     1.8 +theory If imports "~~/src/FOL/FOL" begin
     1.9  
    1.10  definition "if" :: "[o,o,o]=>o" where
    1.11    "if(P,Q,R) == P&Q | ~P&R"