src/HOL/IsaMakefile
changeset 17323 2fc68de9de1f
parent 17308 5d9bbc0d9bd3
child 17330 e007b307a09e
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 12 15:52:00 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Sep 12 16:20:18 2005 +0200
     1.3 @@ -245,6 +245,11 @@
     1.4    Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \
     1.5    Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
     1.6  
     1.7 +IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
     1.8 +  Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
     1.9 +  Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
    1.10 +  Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
    1.11 +
    1.12  HOL-Complex-Import: HOL-Complex $(LOG)/HOL-Complex-Import.gz
    1.13  
    1.14  $(LOG)/HOL-Complex-Import.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES)
    1.15 @@ -261,6 +266,11 @@
    1.16    Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
    1.17  	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOL
    1.18  
    1.19 +HOL-Complex-Generate-HOLLight: HOL-Complex $(LOG)/HOL-Complex-Generate-HOLLight.gz
    1.20 +
    1.21 +$(LOG)/HOL-Complex-Generate-HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES)  \
    1.22 +  Import/Generate-HOLLight/GenHOLLight.thy Import/Generate-HOLLight/ROOT.ML
    1.23 +	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOLLight
    1.24  
    1.25  ## HOL-Import-HOL
    1.26  
    1.27 @@ -624,29 +634,29 @@
    1.28  
    1.29  ## HOL-Complex-Matrix
    1.30  
    1.31 -HOL-Complex-Matrix: HOL $(LOG)/HOL-Complex-Matrix.gz
    1.32 +#HOL-Complex-Matrix: HOL $(LOG)/HOL-Complex-Matrix.gz
    1.33  
    1.34 -$(LOG)/HOL-Complex-Matrix.gz: $(OUT)/HOL-Complex \
    1.35 +#$(LOG)/HOL-Complex-Matrix.gz: $(OUT)/HOL-Complex \
    1.36 +#  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
    1.37 +#  Matrix/document/root.tex Matrix/ROOT.ML \
    1.38 +#  Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
    1.39 +#  Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
    1.40 +#  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
    1.41 +#  Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
    1.42 +#	@$(ISATOOL) usedir $(OUT)/HOL-Complex Matrix
    1.43 +
    1.44 +## HOL-Complex-Matrix
    1.45 +
    1.46 +HOL-Complex-Matrix: HOL $(OUT)/HOL-Complex-Matrix
    1.47 +
    1.48 +$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
    1.49    Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
    1.50    Matrix/document/root.tex Matrix/ROOT.ML \
    1.51    Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
    1.52    Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
    1.53    Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
    1.54    Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
    1.55 -	@$(ISATOOL) usedir $(OUT)/HOL-Complex Matrix
    1.56 -
    1.57 -## HOL-Complex-Matrix
    1.58 -
    1.59 -#HOL-Complex-Matrix: HOL $(OUT)/HOL-Complex-Matrix
    1.60 -#
    1.61 -#$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
    1.62 -#  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
    1.63 -#  Matrix/document/root.tex Matrix/ROOT.ML \
    1.64 -#  Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
    1.65 -#  Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
    1.66 -#  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
    1.67 -#  Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
    1.68 -#	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
    1.69 +	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
    1.70  
    1.71  
    1.72  ## TLA