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