src/HOL/IsaMakefile
changeset 17489 f70d62d5f9c8
parent 17488 67376a311a2b
child 17507 507e519a0dad
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 19 18:30:22 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Sep 19 19:49:09 2005 +0200
     1.3 @@ -639,25 +639,12 @@
     1.4  
     1.5  ## HOL-Complex-Matrix
     1.6  
     1.7 -#HOL-Complex-Matrix: HOL $(LOG)/HOL-Complex-Matrix.gz
     1.8 -
     1.9 -#$(LOG)/HOL-Complex-Matrix.gz: $(OUT)/HOL-Complex \
    1.10 -#  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
    1.11 -#  Matrix/document/root.tex Matrix/ROOT.ML \
    1.12 -#  Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
    1.13 -#  Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
    1.14 -#  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
    1.15 -#  Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
    1.16 -#	@$(ISATOOL) usedir $(OUT)/HOL-Complex Matrix
    1.17 -
    1.18 -## HOL-Complex-Matrix
    1.19 -
    1.20  HOL-Complex-Matrix: HOL $(OUT)/HOL-Complex-Matrix
    1.21  
    1.22  $(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
    1.23    Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
    1.24    Matrix/document/root.tex Matrix/ROOT.ML \
    1.25 -  Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
    1.26 +  Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
    1.27    Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
    1.28    Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
    1.29    Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML