diff -r afe750876848 -r ac9b58304d62 src/FOL/ex/ROOT.ML
--- a/src/FOL/ex/ROOT.ML	Wed Mar 06 10:05:00 1996 +0100
+++ b/src/FOL/ex/ROOT.ML	Wed Mar 06 10:14:47 1996 +0100
@@ -37,5 +37,9 @@
 time_use_thy "Nat2";
 time_use_thy "List";
 
+writeln"\n** How to declare an oracle **\n";
+time_use_thy "IffOracle";
+
+
 cd "..";
 maketest"END: Root file for FOL examples";