| changeset 45865 | 7887eabb1997 |
| parent 45864 | a8b9191609a8 |
| parent 45863 | afdb92130f5a |
| child 45870 | 347c9383acd8 |
--- a/Admin/Benchmarks/HOL-record/ROOT.ML Wed Dec 14 15:05:22 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* Title: Admin/Benchmarks/HOL-record/ROOT.ML - -Some benchmark on large record. -*) - -val tests = ["Record_Benchmark"]; - -Toplevel.timing := true; - -warning "\nset quick_and_dirty\n"; quick_and_dirty := true; -use_thys tests; - -warning "\nreset quick_and_dirty\n"; quick_and_dirty := false; -use_thys tests;