src/HOL/IsaMakefile
changeset 27484 dbb9981c3d18
parent 27480 02d5a9603bd9
child 27624 a925aa66e17a
equal deleted inserted replaced
27483:7c58324cd418 27484:dbb9981c3d18
   818   $(SRC)/Tools/Compute_Oracle/am_interpreter.ML				\
   818   $(SRC)/Tools/Compute_Oracle/am_interpreter.ML				\
   819   $(SRC)/Tools/Compute_Oracle/am.ML					\
   819   $(SRC)/Tools/Compute_Oracle/am.ML					\
   820   $(SRC)/Tools/Compute_Oracle/linker.ML					\
   820   $(SRC)/Tools/Compute_Oracle/linker.ML					\
   821   $(SRC)/Tools/Compute_Oracle/am_ghc.ML					\
   821   $(SRC)/Tools/Compute_Oracle/am_ghc.ML					\
   822   $(SRC)/Tools/Compute_Oracle/am_sml.ML					\
   822   $(SRC)/Tools/Compute_Oracle/am_sml.ML					\
   823   $(SRC)/Tools/Compute_Oracle/compute.ML Matrix/MatrixGeneral.thy	\
   823   $(SRC)/Tools/Compute_Oracle/compute.ML	\
   824   Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy		\
   824   Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy		\
   825   Matrix/document/root.tex Matrix/ROOT.ML Matrix/cplex/Cplex.thy	\
   825   Matrix/document/root.tex Matrix/ROOT.ML Matrix/cplex/Cplex.thy	\
   826   Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML	\
   826   Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML	\
   827   Matrix/cplex/FloatSparseMatrix.thy					\
       
   828   Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML	\
   827   Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML	\
   829   Matrix/cplex/MatrixLP.thy Matrix/cplex/matrixlp.ML
   828   Matrix/cplex/matrixlp.ML
   830 	@$(ISATOOL) usedir -g true $(OUT)/HOL Matrix
   829 	@$(ISATOOL) usedir -g true $(OUT)/HOL Matrix
   831 
   830 
   832 
   831 
   833 ## TLA
   832 ## TLA
   834 
   833