src/HOL/Record_Benchmark/ROOT.ML
author wenzelm
Tue, 03 Apr 2012 20:08:08 +0200
changeset 47314 644a3b74cfd0
parent 45860 93eda35a8377
permissions -rw-r--r--
less intrusive visibility;
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"];