# HG changeset patch
# User obua
# Date 1126534818 -7200
# Node ID 2fc68de9de1f8beb6f6a037db790f966daeb4584
# Parent  781abf7011e6efd2b7bf193e45bb4fe22395b751
1) Added target HOL-Complex-Generate-HOLLight
2) Make heap image for HOL-Complex-Matrix

diff -r 781abf7011e6 -r 2fc68de9de1f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Sep 12 15:52:00 2005 +0200
+++ b/src/HOL/IsaMakefile	Mon Sep 12 16:20:18 2005 +0200
@@ -245,6 +245,11 @@
   Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \
   Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
 
+IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
+  Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
+  Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
+  Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
+
 HOL-Complex-Import: HOL-Complex $(LOG)/HOL-Complex-Import.gz
 
 $(LOG)/HOL-Complex-Import.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES)
@@ -261,6 +266,11 @@
   Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
 	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOL
 
+HOL-Complex-Generate-HOLLight: HOL-Complex $(LOG)/HOL-Complex-Generate-HOLLight.gz
+
+$(LOG)/HOL-Complex-Generate-HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES)  \
+  Import/Generate-HOLLight/GenHOLLight.thy Import/Generate-HOLLight/ROOT.ML
+	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOLLight
 
 ## HOL-Import-HOL
 
@@ -624,29 +634,29 @@
 
 ## HOL-Complex-Matrix
 
-HOL-Complex-Matrix: HOL $(LOG)/HOL-Complex-Matrix.gz
+#HOL-Complex-Matrix: HOL $(LOG)/HOL-Complex-Matrix.gz
 
-$(LOG)/HOL-Complex-Matrix.gz: $(OUT)/HOL-Complex \
+#$(LOG)/HOL-Complex-Matrix.gz: $(OUT)/HOL-Complex \
+#  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
+#  Matrix/document/root.tex Matrix/ROOT.ML \
+#  Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
+#  Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
+#  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
+#  Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
+#	@$(ISATOOL) usedir $(OUT)/HOL-Complex Matrix
+
+## HOL-Complex-Matrix
+
+HOL-Complex-Matrix: HOL $(OUT)/HOL-Complex-Matrix
+
+$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
   Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
   Matrix/document/root.tex Matrix/ROOT.ML \
   Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
   Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
   Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
   Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
-	@$(ISATOOL) usedir $(OUT)/HOL-Complex Matrix
-
-## HOL-Complex-Matrix
-
-#HOL-Complex-Matrix: HOL $(OUT)/HOL-Complex-Matrix
-#
-#$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
-#  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
-#  Matrix/document/root.tex Matrix/ROOT.ML \
-#  Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
-#  Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
-#  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
-#  Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
-#	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
+	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
 
 
 ## TLA