--- a/ex/ROOT.ML Sun Oct 17 17:23:51 1993 +0100
+++ b/ex/ROOT.ML Sun Oct 17 17:33:40 1993 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/ex/ROOT
+(* Title: HOL/ex/ROOT
ID: $Id$
Author: Tobias Nipkow, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -13,11 +13,11 @@
time_use "ex/cla.ML";
time_use "ex/meson.ML";
time_use "ex/meson-test.ML";
-time_use_thy "ex/lex-prod";
+time_use_thy "ex/lexprod";
time_use_thy "ex/puzzle";
time_use "ex/set.ML";
time_use_thy "ex/finite";
-time_use_thy "ex/prop-log";
+time_use_thy "ex/pl";
time_use_thy "ex/term";
time_use_thy "ex/simult";
maketest "END: Root file for HOL examples";