(* Title: HOL/Import/ROOT.ML ID: $Id$ Author: Sebastian Skalberg (TU Muenchen) *) use_thy "HOL4Compat"; use_thy "HOL4Syntax";