(* Title: HOL/Import/ROOT.ML Author: Sebastian Skalberg (TU Muenchen) *) use_thys ["HOL4Compat", "HOL4Syntax"];