--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Aug 27 10:49:12 1999 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Aug 27 10:54:31 1999 +0200
@@ -1,10 +1,16 @@
-(* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy
+(* Title: Admin/Benchmarks/HOL-datatype/ROOT.ML
ID: $Id$
Some rather large datatype examples (from John Harrison).
*)
-time_use_thy "Brackin";
-time_use_thy "Instructions";
-time_use_thy "SML";
-time_use_thy "Verilog";
+val tests = ["Brackin", "Instructions", "SML", "Verilog"];
+
+set Toplevel.trace;
+
+warning "\nset quick_and_dirty\n"; set quick_and_dirty;
+seq time_use_thy tests;
+
+warning "\nreset quick_and_dirty\n"; reset quick_and_dirty;
+seq remove_thy tests;
+seq time_use_thy tests;