1 (* Title: HOL/Import/HOLLight/ROOT.ML
2 ID: $Id$
3 *)
4
5 use_thy "HOLLight";
1 use_thy "HOLLight";