src/HOL/IsaMakefile
changeset 16873 9ed940a1bebb
parent 16784 92ff7c903585
child 16908 d374530bfaaa
     1.1 --- a/src/HOL/IsaMakefile	Tue Jul 19 14:59:11 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Jul 19 16:16:53 2005 +0200
     1.3 @@ -630,9 +630,23 @@
     1.4    Matrix/document/root.tex Matrix/ROOT.ML \
     1.5    Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
     1.6    Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
     1.7 -  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML
     1.8 +  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
     1.9 +  Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
    1.10  	@$(ISATOOL) usedir $(OUT)/HOL-Complex Matrix
    1.11  
    1.12 +## HOL-Complex-Matrix
    1.13 +
    1.14 +#HOL-Complex-Matrix: HOL $(OUT)/HOL-Complex-Matrix
    1.15 +#
    1.16 +#$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
    1.17 +#  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
    1.18 +#  Matrix/document/root.tex Matrix/ROOT.ML \
    1.19 +#  Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
    1.20 +#  Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
    1.21 +#  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
    1.22 +#  Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
    1.23 +#	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
    1.24 +
    1.25  
    1.26  ## TLA
    1.27