src/HOL/Record_Benchmark/ROOT.ML
author wenzelm
Sun, 20 May 2012 11:34:33 +0200
changeset 47884 21c42b095c84
parent 45860 93eda35a8377
permissions -rw-r--r--
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45860
93eda35a8377 more visible benchmarks;
wenzelm
parents: 44640
diff changeset
     1
(*  Title:      HOL/Record_Benchmark/ROOT.ML
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
     2
33695
bec342db1bf4 eliminated obsolete CVS Ids;
wenzelm
parents: 33693
diff changeset
     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
83dc04ccabd5 repaired benchmarks;
wenzelm
parents: 38798
diff changeset
     6
Toplevel.timing := true;
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
     7
45860
93eda35a8377 more visible benchmarks;
wenzelm
parents: 44640
diff changeset
     8
use_thys ["Record_Benchmark"];