--- 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]} *}
--- 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"