--- 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.
--- 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