(* Title: HOL/Record_Benchmark/ROOT.ML Some benchmark on large record. *) Toplevel.timing := true; use_thys ["Record_Benchmark"];