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