author | berghofe |
Mon, 19 Nov 2001 17:40:45 +0100 | |
changeset 12238 | 09966ccbc84c |
parent 10100 | 567b9676cb0a |
child 15531 | 08c8dad8e399 |
permissions | -rw-r--r-- |
7373 | 1 |
(* Title: Admin/Benchmarks/HOL-datatype/ROOT.ML |
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
2 |
ID: $Id$ |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
3 |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
4 |
Some rather large datatype examples (from John Harrison). |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
5 |
*) |
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
6 |
|
7373 | 7 |
val tests = ["Brackin", "Instructions", "SML", "Verilog"]; |
8 |
||
9000 | 9 |
set timing; |
7373 | 10 |
|
11 |
warning "\nset quick_and_dirty\n"; set quick_and_dirty; |
|
12 |
seq time_use_thy tests; |
|
13 |
||
10100 | 14 |
(* not run by default |
7373 | 15 |
warning "\nreset quick_and_dirty\n"; reset quick_and_dirty; |
16 |
seq remove_thy tests; |
|
17 |
seq time_use_thy tests; |
|
10100 | 18 |
*) |