| changeset 45865 | 7887eabb1997 |
| parent 45864 | a8b9191609a8 |
| parent 45863 | afdb92130f5a |
| child 45870 | 347c9383acd8 |
| 45864:a8b9191609a8 | 45865:7887eabb1997 |
|---|---|
1 (* Title: Admin/Benchmarks/HOL-datatype/ROOT.ML |
|
2 |
|
3 Some rather large datatype examples (from John Harrison). |
|
4 *) |
|
5 |
|
6 val tests = ["Brackin", "Instructions", "SML", "Verilog"]; |
|
7 |
|
8 Toplevel.timing := true; |
|
9 |
|
10 warning "\nset quick_and_dirty\n"; quick_and_dirty := true; |
|
11 use_thys tests; |
|
12 |
|
13 warning "\nreset quick_and_dirty\n"; quick_and_dirty := false; |
|
14 List.app Thy_Info.remove_thy tests; |
|
15 use_thys tests; |