only run quick_and_dirty version by default;
authorwenzelm
Thu, 28 Sep 2000 14:35:23 +0200
changeset 10100 567b9676cb0a
parent 10099 44da60e5331b
child 10101 746263fbcbfd
only run quick_and_dirty version by default;
Admin/Benchmarks/HOL-datatype/ROOT.ML
--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML	Thu Sep 28 14:34:49 2000 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML	Thu Sep 28 14:35:23 2000 +0200
@@ -11,6 +11,8 @@
 warning "\nset quick_and_dirty\n"; set quick_and_dirty;
 seq time_use_thy tests;
 
+(* not run by default
 warning "\nreset quick_and_dirty\n"; reset quick_and_dirty;
 seq remove_thy tests;
 seq time_use_thy tests;
+*)