src/Sequents/LK/ROOT.ML

--- a/src/Sequents/LK/ROOT.ML	Tue May 30 16:03:09 2000 +0200
+++ b/src/Sequents/LK/ROOT.ML	Tue May 30 16:08:38 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      LK/ex/ROOT
+(*  Title:      LK/ex/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1992  University of Cambridge
@@ -6,10 +6,7 @@
 Executes all examples for Classical Logic. 
 *)
 
-writeln"Root file for LK examples";
-
-set proof_timing;
 time_use "prop.ML";
 time_use "quant.ML";
 time_use "hardquant.ML";
-use_thy "Nat";
+time_use_thy "Nat";