author | nipkow |
Fri, 24 Mar 2000 08:56:48 +0100 | |
changeset 8563 | 2746bc9a7ef2 |
parent 7373 | 776d888472aa |
child 9000 | c20d58286a51 |
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 |
||
9 |
set Toplevel.trace; |
|
10 |
||
11 |
warning "\nset quick_and_dirty\n"; set quick_and_dirty; |
|
12 |
seq time_use_thy tests; |
|
13 |
||
14 |
warning "\nreset quick_and_dirty\n"; reset quick_and_dirty; |
|
15 |
seq remove_thy tests; |
|
16 |
seq time_use_thy tests; |