src/HOL/Record_Benchmark/ROOT.ML
author wenzelm
Mon, 25 Jun 2012 11:07:51 +0200
changeset 48120 9fe0e71052a0
parent 45860 93eda35a8377
permissions -rw-r--r--
updated "isar-ref" manual, reduced remaining material in "ref" manual.
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"];