Theory HOL_Light_Import

(*  Title:      HOL/Import/HOL_Light_Import.thy
    Author:     Cezary Kaliszyk, University of Innsbruck
    Author:     Alexander Krauss, QAware GmbH
*)

section ‹Main HOL Light importer›

theory HOL_Light_Import
  imports HOL_Light_Maps
  options [condition = "$HOL_LIGHT_BUNDLE"]
begin

import_file "$HOL_LIGHT_BUNDLE"

end