Admin/Benchmarks/HOL-record/ROOT.ML
author wenzelm
Wed, 21 Jul 2010 17:55:07 +0200
changeset 37900 8b3498b9eb4b
parent 33695 bec342db1bf4
child 38798 89f273ab1d42
permissions -rw-r--r--
recovered benchmarks, which are not tested automatically;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
     1
(*  Title:      Admin/Benchmarks/HOL-record/ROOT.ML
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
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
     6
val tests = ["RecordBenchmark"];
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
     7
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
     8
Unsynchronized.set timing;
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
     9
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
    10
warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty;
37900
8b3498b9eb4b recovered benchmarks, which are not tested automatically;
wenzelm
parents: 33695
diff changeset
    11
use_thys tests;
33693
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
    12
9d76c8080aea added benchmark for large records
schirmer <schirmer@in.tum.de>
parents:
diff changeset
    13
warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty;
37900
8b3498b9eb4b recovered benchmarks, which are not tested automatically;
wenzelm
parents: 33695
diff changeset
    14
use_thys tests;