# HG changeset patch
# User krauss
# Date 1333312916 -7200
# Node ID 6488c5efec49e0a900f9763d7f519003c73f8076
# Parent  3b9eeb4a2967982b91b5e48aeec6d34ec5425b15
renamed import session back to Import, conforming to directory name; NEWS

diff -r 3b9eeb4a2967 -r 6488c5efec49 NEWS
--- a/NEWS	Sun Apr 01 22:14:59 2012 +0200
+++ b/NEWS	Sun Apr 01 22:41:56 2012 +0200
@@ -135,6 +135,10 @@
 * Code generation by default implements sets as container type rather
 than predicates.  INCOMPATIBILITY.
 
+* New proof import from HOL Light, cf. HOL/Import. Requires a proof
+bundle, which is available as an external component. Removed old (and
+mostly dead) Importer for HOL4 and HOL Light.  INCOMPATIBILITY.
+
 * New type synonym 'a rel = ('a * 'a) set
 
 * Theory Divides: Discontinued redundant theorems about div and mod.
diff -r 3b9eeb4a2967 -r 6488c5efec49 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Apr 01 22:14:59 2012 +0200
+++ b/src/HOL/IsaMakefile	Sun Apr 01 22:41:56 2012 +0200
@@ -38,8 +38,8 @@
       HOLCF-Library \
       HOLCF-Tutorial \
       HOLCF-ex \
-  HOL-HOL_Light \
   HOL-IMPP \
+  HOL-Import \
   HOL-IOA \
       IOA-ABP \
       IOA-NTP \
@@ -550,16 +550,16 @@
 
 ## Import sessions
 
-HOL-HOL_Light: $(LOG)/HOL-HOL_Light.gz
+HOL-Import: $(LOG)/HOL-Import.gz
 
-$(LOG)/HOL-HOL_Light.gz: $(OUT)/HOL \
+$(LOG)/HOL-Import.gz: $(OUT)/HOL \
   Import/ROOT.ML \
   Import/Import_Setup.thy \
   Import/import_data.ML \
   Import/import_rule.ML \
   Import/HOL_Light_Maps.thy \
   Import/HOL_Light_Import.thy
-	@cd Import; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-HOL_Light
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Import
 
 ## HOL-Number_Theory