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";