| author | huffman |
| Wed, 10 Nov 2010 18:45:48 -0800 | |
| changeset 40506 | 4c5363173f88 |
| parent 38798 | 89f273ab1d42 |
| child 44639 | 83dc04ccabd5 |
| 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 |
|
|
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset
|
3 |
Some rather large datatype examples (from John Harrison). |
|
7013
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
4 |
*) |
|
8a7fb425e04a
Some rather large datatype examples (from John Harrison).
berghofe
parents:
diff
changeset
|
5 |
|
| 7373 | 6 |
val tests = ["Brackin", "Instructions", "SML", "Verilog"]; |
7 |
||
|
38798
89f273ab1d42
expanded some aliases from structure Unsynchronized;
wenzelm
parents:
37875
diff
changeset
|
8 |
timing := true; |
| 7373 | 9 |
|
|
38798
89f273ab1d42
expanded some aliases from structure Unsynchronized;
wenzelm
parents:
37875
diff
changeset
|
10 |
warning "\nset quick_and_dirty\n"; quick_and_dirty := true; |
|
37875
496d723516e6
recovered benchmarks, which are not tested automatically;
wenzelm
parents:
32871
diff
changeset
|
11 |
use_thys tests; |
| 7373 | 12 |
|
|
38798
89f273ab1d42
expanded some aliases from structure Unsynchronized;
wenzelm
parents:
37875
diff
changeset
|
13 |
warning "\nreset quick_and_dirty\n"; quick_and_dirty := false; |
|
37875
496d723516e6
recovered benchmarks, which are not tested automatically;
wenzelm
parents:
32871
diff
changeset
|
14 |
List.app Thy_Info.remove_thy tests; |
|
496d723516e6
recovered benchmarks, which are not tested automatically;
wenzelm
parents:
32871
diff
changeset
|
15 |
use_thys tests; |