| author | wenzelm |
| Sun, 09 Oct 2011 16:47:58 +0200 | |
| changeset 45107 | 76fef3e57004 |
| parent 44640 | 3e666dcdcd32 |
| 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 |
|
| 44640 | 6 |
val tests = ["Record_Benchmark"]; |
|
33693
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
7 |
|
| 44639 | 8 |
Toplevel.timing := true; |
|
33693
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
9 |
|
|
38798
89f273ab1d42
expanded some aliases from structure Unsynchronized;
wenzelm
parents:
37900
diff
changeset
|
10 |
warning "\nset quick_and_dirty\n"; quick_and_dirty := true; |
|
37900
8b3498b9eb4b
recovered benchmarks, which are not tested automatically;
wenzelm
parents:
33695
diff
changeset
|
11 |
use_thys tests; |
|
33693
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
12 |
|
|
38798
89f273ab1d42
expanded some aliases from structure Unsynchronized;
wenzelm
parents:
37900
diff
changeset
|
13 |
warning "\nreset quick_and_dirty\n"; quick_and_dirty := false; |
|
37900
8b3498b9eb4b
recovered benchmarks, which are not tested automatically;
wenzelm
parents:
33695
diff
changeset
|
14 |
use_thys tests; |