1034 |
1034 |
1035 ## HOL-Matrix |
1035 ## HOL-Matrix |
1036 |
1036 |
1037 HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz |
1037 HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz |
1038 |
1038 |
1039 $(LOG)/HOL-Matrix.gz: $(OUT)/HOL \ |
1039 $(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ComputeFloat.thy \ |
1040 $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \ |
1040 Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy \ |
1041 $(SRC)/Tools/Compute_Oracle/am_compiler.ML \ |
1041 Matrix/Compute_Oracle/Compute_Oracle.thy Matrix/Compute_Oracle/am.ML \ |
1042 $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \ |
1042 Matrix/Compute_Oracle/am_compiler.ML Matrix/Compute_Oracle/am_ghc.ML \ |
1043 $(SRC)/Tools/Compute_Oracle/am.ML \ |
1043 Matrix/Compute_Oracle/am_interpreter.ML \ |
1044 $(SRC)/Tools/Compute_Oracle/linker.ML \ |
1044 Matrix/Compute_Oracle/am_sml.ML Matrix/Compute_Oracle/compute.ML \ |
1045 $(SRC)/Tools/Compute_Oracle/am_ghc.ML \ |
1045 Matrix/Compute_Oracle/linker.ML Matrix/Cplex.thy \ |
1046 $(SRC)/Tools/Compute_Oracle/am_sml.ML \ |
|
1047 $(SRC)/Tools/Compute_Oracle/compute.ML Matrix/ComputeFloat.thy \ |
|
1048 Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy Tools/float_arith.ML \ |
|
1049 Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy \ |
|
1050 Matrix/document/root.tex Matrix/ROOT.ML Matrix/Cplex.thy \ |
|
1051 Matrix/CplexMatrixConverter.ML Matrix/Cplex_tools.ML \ |
1046 Matrix/CplexMatrixConverter.ML Matrix/Cplex_tools.ML \ |
1052 Matrix/FloatSparseMatrixBuilder.ML Matrix/fspmlp.ML \ |
1047 Matrix/FloatSparseMatrixBuilder.ML Matrix/LP.thy Matrix/Matrix.thy \ |
1053 Matrix/matrixlp.ML |
1048 Matrix/ROOT.ML Matrix/SparseMatrix.thy Matrix/document/root.tex \ |
|
1049 Matrix/fspmlp.ML Matrix/matrixlp.ML Tools/float_arith.ML |
1054 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix |
1050 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix |
1055 |
1051 |
1056 |
1052 |
1057 ## TLA |
1053 ## TLA |
1058 |
1054 |