src/HOL/Import/ROOT.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/ROOT.ML	Sun Apr 01 14:50:47 2012 +0200
@@ -0,0 +1,5 @@
+use_thy "HOL_Light_Maps";
+
+if getenv "HOL_LIGHT_DUMP" <> ""
+then use_thy "HOL_Light_Import"
+else ()