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