src/HOL/Record_Benchmark/ROOT.ML
author huffman
Fri, 27 Jul 2012 15:42:39 +0200
changeset 48556 62a3fbf9d35b
parent 45860 93eda35a8377
permissions -rw-r--r--
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
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"];