| author | huffman |
| Mon, 26 Apr 2010 15:51:10 -0700 | |
| changeset 36434 | 2a74926bd760 |
| parent 33695 | bec342db1bf4 |
| child 37900 | 8b3498b9eb4b |
| permissions | -rw-r--r-- |
|
33693
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
1 |
(* Title: Admin/Benchmarks/HOL-record/ROOT.ML |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
2 |
|
| 33695 | 3 |
Some benchmark on large record. |
|
33693
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
4 |
*) |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
5 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
6 |
val tests = ["RecordBenchmark"]; |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
7 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
8 |
Unsynchronized.set timing; |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
9 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
10 |
warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty; |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
11 |
List.app time_use_thy tests; |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
12 |
|
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
13 |
warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty; |
|
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
14 |
List.app time_use_thy tests; |