(* Title: HOL/Datatype_Benchmark/ROOT.ML Some rather large datatype examples (from John Harrison). *) Toplevel.timing := true; use_thys ["Brackin", "Instructions", "SML", "Verilog"];