--- a/NEWS Thu Feb 21 18:27:28 2013 +0100
+++ b/NEWS Fri Feb 22 14:25:52 2013 +0100
@@ -6,6 +6,9 @@
*** HOL ***
+* Discontinued obsolete src/HOL/IsaMakefile (considered legacy since
+Isabelle2013). Use "isabelle build" to operate on Isabelle sessions.
+
* Numeric types mapped by default to target language numerals:
natural (replaces former code_numeral) and integer (replaces
former code_int). Conversions are available as integer_of_natural /
--- a/src/HOL/IsaMakefile Thu Feb 21 18:27:28 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,66 +0,0 @@
-#
-# approximative IsaMakefile for legacy applications
-#
-
-default: HOL
-
-clean:
- -@$(ISABELLE_TOOL) build -a -n -c
-
-all:
- @$(ISABELLE_TOOL) build -a
-
-
-Pure: $(ISABELLE_OUTPUT)/Pure
-
-$(ISABELLE_OUTPUT)/Pure:
- @$(ISABELLE_TOOL) build -b Pure
-
-
-HOL: $(ISABELLE_OUTPUT)/HOL
-
-$(ISABELLE_OUTPUT)/HOL:
- @$(ISABELLE_TOOL) build -b HOL
-
-
-HOL-Library: $(ISABELLE_OUTPUT)/HOL-Library
-
-$(ISABELLE_OUTPUT)/HOL-Library:
- @$(ISABELLE_TOOL) build -b HOL-Library
-
-
-HOL-IMP: $(ISABELLE_OUTPUT)/HOL-IMP
-
-$(ISABELLE_OUTPUT)/HOL-IMP:
- @$(ISABELLE_TOOL) build -b HOL-IMP
-
-
-HOL-Multivariate_Analysis: $(ISABELLE_OUTPUT)/HOL-Multivariate_Analysis
-
-$(ISABELLE_OUTPUT)/HOL-Multivariate_Analysis:
- @$(ISABELLE_TOOL) build -b HOL-Multivariate_Analysis
-
-
-HOL-Probability: $(ISABELLE_OUTPUT)/HOL-Probability
-
-$(ISABELLE_OUTPUT)/HOL-Probability:
- @$(ISABELLE_TOOL) build -b HOL-Probability
-
-
-HOL-Nominal: $(ISABELLE_OUTPUT)/HOL-Nominal
-
-$(ISABELLE_OUTPUT)/HOL-Nominal:
- @$(ISABELLE_TOOL) build -b HOL-Nominal
-
-
-HOL-Word: $(ISABELLE_OUTPUT)/HOL-Word
-
-$(ISABELLE_OUTPUT)/HOL-Word:
- @$(ISABELLE_TOOL) build -b HOL-Word
-
-
-HOLCF: $(ISABELLE_OUTPUT)/HOLCF
-
-$(ISABELLE_OUTPUT)/HOLCF:
- @$(ISABELLE_TOOL) build -b HOLCF
-