merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)

--- a/Admin/contributed_components	Sun Apr 01 23:07:15 2012 +0200
+++ b/Admin/contributed_components	Sun Apr 01 23:21:54 2012 +0200
@@ -1,6 +1,7 @@
 #contributed components
 contrib/cvc3-2.2
 contrib/e-1.4
+contrib/hol-light-bundle-0.5-126
 contrib/kodkodi-1.2.16
 contrib/spass-3.7
 contrib/scala-2.8.1.final

--- a/Admin/update-keywords	Sun Apr 01 23:07:15 2012 +0200
+++ b/Admin/update-keywords	Sun Apr 01 23:21:54 2012 +0200
@@ -13,7 +13,7 @@
 isabelle keywords \
   "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
   "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \
-  "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-HOL_Light.gz"
+  "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
 
 isabelle keywords -k ZF \
   "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"

--- a/CONTRIBUTORS	Sun Apr 01 23:07:15 2012 +0200
+++ b/CONTRIBUTORS	Sun Apr 01 23:21:54 2012 +0200
@@ -6,9 +6,13 @@
 Contributions to this Isabelle version
 --------------------------------------
 
-* January 2011: Florian Haftmann, TUM, et. al.
+* January 2012: Florian Haftmann, TUM, et. al.
   (Re-)Introduction of the "set" type constructor.
 
+* March 2012: Cezary Kaliszyk, University of Innsbruck and
+  Alexander Krauss, QAware GmbH
+  Faster and more scalable Import mechanism for HOL Light proofs.
+
 
 Contributions to Isabelle2011-1
 -------------------------------

--- a/NEWS	Sun Apr 01 23:07:15 2012 +0200
+++ b/NEWS	Sun Apr 01 23:21:54 2012 +0200
@@ -135,6 +135,11 @@
 * Code generation by default implements sets as container type rather
 than predicates.  INCOMPATIBILITY.
 
+* New proof import from HOL Light: Faster, simpler, and more scalable.
+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/etc/isar-keywords.el	Sun Apr 01 23:07:15 2012 +0200
+++ b/etc/isar-keywords.el	Sun Apr 01 23:21:54 2012 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-HOL_Light.
+;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 

--- a/src/HOL/Import/HOL_Light_Import.thy	Sun Apr 01 23:07:15 2012 +0200
+++ b/src/HOL/Import/HOL_Light_Import.thy	Sun Apr 01 23:21:54 2012 +0200
@@ -9,7 +9,7 @@
 imports HOL_Light_Maps
 begin
 
-import_file "$HOL_LIGHT_DUMP"
+import_file "$HOL_LIGHT_BUNDLE"
 
 end
 

--- a/src/HOL/Import/ROOT.ML	Sun Apr 01 23:07:15 2012 +0200
+++ b/src/HOL/Import/ROOT.ML	Sun Apr 01 23:21:54 2012 +0200
@@ -1,5 +1,5 @@
 use_thy "HOL_Light_Maps";
 
-if getenv "HOL_LIGHT_DUMP" <> ""
+if getenv "HOL_LIGHT_BUNDLE" <> ""
 then use_thy "HOL_Light_Import"
 else ()

--- a/src/HOL/IsaMakefile	Sun Apr 01 23:07:15 2012 +0200
+++ b/src/HOL/IsaMakefile	Sun Apr 01 23:21:54 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 \
@@ -548,18 +548,18 @@
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
 
 
-## HOL-HOL_Light
+## HOL-Import
 
-HOL-HOL_Light: $(OUT)/HOL-HOL_Light
+HOL-Import: $(LOG)/HOL-Import.gz
 
-$(OUT)/HOL-HOL_Light: $(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