(* Title: HOL/Import/Generate-HOLLight/ROOT.ML ID: $Id$ Author: Steven Obua and Sebastian Skalberg (TU Muenchen) *) use_thy "GenHOLLight";