src/FOL/ex/ROOT.ML
changeset 1549 ac9b58304d62
parent 1459 d12da312eff4
child 2236 c7869a443b14
--- 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";