| changeset 33695 | bec342db1bf4 |
| parent 33693 | 9d76c8080aea |
| child 37900 | 8b3498b9eb4b |
| 33694:f06fe9c2152d | 33695:bec342db1bf4 |
|---|---|
1 (* Title: Admin/Benchmarks/HOL-record/ROOT.ML |
1 (* Title: Admin/Benchmarks/HOL-record/ROOT.ML |
2 |
2 |
3 Some benchmark on large record |
3 Some benchmark on large record. |
4 *) |
4 *) |
5 |
5 |
6 val tests = ["RecordBenchmark"]; |
6 val tests = ["RecordBenchmark"]; |
7 |
7 |
8 Unsynchronized.set timing; |
8 Unsynchronized.set timing; |