ex/ROOT.ML

-(*  Title: 	HOL/ex/ROOT
+(*  Title:  	HOL/ex/ROOT
     ID:         $Id$
     Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
 Executes all examples for Higher-Order Logic. 

 writeln"Root file for HOL examples";
 proof_timing := true;
 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";