(* Title: Admin/Benchmarks/HOL-datatype/Brackin.thy ID: $Id$ Some rather large datatype examples (from John Harrison). *) time_use_thy "Brackin"; time_use_thy "Instructions"; time_use_thy "SML"; time_use_thy "Verilog";