| author | wenzelm |
| Tue, 03 Apr 2012 20:08:08 +0200 | |
| changeset 47314 | 644a3b74cfd0 |
| parent 45860 | 93eda35a8377 |
| permissions | -rw-r--r-- |
| 45860 | 1 |
(* Title: HOL/Record_Benchmark/ROOT.ML |
|
33693
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 |
|
| 44639 | 6 |
Toplevel.timing := true; |
|
33693
9d76c8080aea
added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff
changeset
|
7 |
|
| 45860 | 8 |
use_thys ["Record_Benchmark"]; |