src/FOL/ex/ROOT.ML
changeset 9205 f171fa6a0989
parent 9000 c20d58286a51
child 11675 c87d695f4adb
--- a/src/FOL/ex/ROOT.ML	Thu Jun 29 22:39:57 2000 +0200
+++ b/src/FOL/ex/ROOT.ML	Thu Jun 29 22:48:08 2000 +0200
@@ -12,7 +12,7 @@
 time_use_thy "Prolog";
 
 writeln"\n** Intuitionistic examples **\n";
-time_use     "int.ML";
+time_use_thy "int";
 
 val thy = IFOL.thy  and  tac = IntPr.fast_tac 1;
 time_use     "prop.ML";