renamed import session back to Import, conforming to directory name; NEWS
authorkrauss
Sun Apr 01 22:41:56 2012 +0200 (2012-04-01)
changeset 472646488c5efec49
parent 47260 3b9eeb4a2967
child 47265 b8c98d476805
renamed import session back to Import, conforming to directory name; NEWS
NEWS
src/HOL/IsaMakefile
     1.1 --- a/NEWS	Sun Apr 01 22:14:59 2012 +0200
     1.2 +++ b/NEWS	Sun Apr 01 22:41:56 2012 +0200
     1.3 @@ -135,6 +135,10 @@
     1.4  * Code generation by default implements sets as container type rather
     1.5  than predicates.  INCOMPATIBILITY.
     1.6  
     1.7 +* New proof import from HOL Light, cf. HOL/Import. Requires a proof
     1.8 +bundle, which is available as an external component. Removed old (and
     1.9 +mostly dead) Importer for HOL4 and HOL Light.  INCOMPATIBILITY.
    1.10 +
    1.11  * New type synonym 'a rel = ('a * 'a) set
    1.12  
    1.13  * Theory Divides: Discontinued redundant theorems about div and mod.
     2.1 --- a/src/HOL/IsaMakefile	Sun Apr 01 22:14:59 2012 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Sun Apr 01 22:41:56 2012 +0200
     2.3 @@ -38,8 +38,8 @@
     2.4        HOLCF-Library \
     2.5        HOLCF-Tutorial \
     2.6        HOLCF-ex \
     2.7 -  HOL-HOL_Light \
     2.8    HOL-IMPP \
     2.9 +  HOL-Import \
    2.10    HOL-IOA \
    2.11        IOA-ABP \
    2.12        IOA-NTP \
    2.13 @@ -550,16 +550,16 @@
    2.14  
    2.15  ## Import sessions
    2.16  
    2.17 -HOL-HOL_Light: $(LOG)/HOL-HOL_Light.gz
    2.18 +HOL-Import: $(LOG)/HOL-Import.gz
    2.19  
    2.20 -$(LOG)/HOL-HOL_Light.gz: $(OUT)/HOL \
    2.21 +$(LOG)/HOL-Import.gz: $(OUT)/HOL \
    2.22    Import/ROOT.ML \
    2.23    Import/Import_Setup.thy \
    2.24    Import/import_data.ML \
    2.25    Import/import_rule.ML \
    2.26    Import/HOL_Light_Maps.thy \
    2.27    Import/HOL_Light_Import.thy
    2.28 -	@cd Import; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-HOL_Light
    2.29 +	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Import
    2.30  
    2.31  ## HOL-Number_Theory
    2.32