src/HOL/IsaMakefile
changeset 17489 f70d62d5f9c8
parent 17488 67376a311a2b
child 17507 507e519a0dad
equal deleted inserted replaced
17488:67376a311a2b 17489:f70d62d5f9c8
   637 	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
   637 	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
   638 
   638 
   639 
   639 
   640 ## HOL-Complex-Matrix
   640 ## HOL-Complex-Matrix
   641 
   641 
   642 #HOL-Complex-Matrix: HOL $(LOG)/HOL-Complex-Matrix.gz
       
   643 
       
   644 #$(LOG)/HOL-Complex-Matrix.gz: $(OUT)/HOL-Complex \
       
   645 #  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
       
   646 #  Matrix/document/root.tex Matrix/ROOT.ML \
       
   647 #  Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
       
   648 #  Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
       
   649 #  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
       
   650 #  Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
       
   651 #	@$(ISATOOL) usedir $(OUT)/HOL-Complex Matrix
       
   652 
       
   653 ## HOL-Complex-Matrix
       
   654 
       
   655 HOL-Complex-Matrix: HOL $(OUT)/HOL-Complex-Matrix
   642 HOL-Complex-Matrix: HOL $(OUT)/HOL-Complex-Matrix
   656 
   643 
   657 $(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
   644 $(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
   658   Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
   645   Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
   659   Matrix/document/root.tex Matrix/ROOT.ML \
   646   Matrix/document/root.tex Matrix/ROOT.ML \
   660   Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
   647   Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
   661   Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
   648   Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
   662   Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
   649   Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
   663   Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
   650   Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
   664 	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
   651 	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
   665 
   652