author | wenzelm |
Thu, 28 Sep 2000 14:35:23 +0200 | |
changeset 10100 | 567b9676cb0a |
parent 10099 | 44da60e5331b |
child 10101 | 746263fbcbfd |
--- 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; +*)