diff -r a7f85074c169 -r 880e587eee9f src/HOL/Import/HOL_Light_Import.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL_Light_Import.thy	Sun Apr 01 14:50:47 2012 +0200
@@ -0,0 +1,15 @@
+(*  Title:      HOL/Import/HOL_Light_Import.thy
+    Author:     Cezary Kaliszyk, University of Innsbruck
+    Author:     Alexander Krauss, QAware GmbH
+*)
+
+header {* Main HOL Light importer *}
+
+theory HOL_Light_Import
+imports HOL_Light_Maps
+begin
+
+import_file "$HOL_LIGHT_DUMP"
+
+end
+