938 |
938 |
939 ## HOL-Matrix |
939 ## HOL-Matrix |
940 |
940 |
941 HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz |
941 HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz |
942 |
942 |
943 $(LOG)/HOL-Matrix.gz: $(OUT)/HOL \ |
943 $(LOG)/HOL-Matrix.gz: $(OUT)/HOL \ |
944 $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \ |
944 $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \ |
945 $(SRC)/Tools/Compute_Oracle/am_compiler.ML \ |
945 $(SRC)/Tools/Compute_Oracle/am_compiler.ML \ |
946 $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \ |
946 $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \ |
947 $(SRC)/Tools/Compute_Oracle/am.ML \ |
947 $(SRC)/Tools/Compute_Oracle/am.ML \ |
948 $(SRC)/Tools/Compute_Oracle/linker.ML \ |
948 $(SRC)/Tools/Compute_Oracle/linker.ML \ |
949 $(SRC)/Tools/Compute_Oracle/am_ghc.ML \ |
949 $(SRC)/Tools/Compute_Oracle/am_ghc.ML \ |
950 $(SRC)/Tools/Compute_Oracle/am_sml.ML \ |
950 $(SRC)/Tools/Compute_Oracle/am_sml.ML \ |
951 $(SRC)/Tools/Compute_Oracle/compute.ML \ |
951 $(SRC)/Tools/Compute_Oracle/compute.ML Matrix/ComputeFloat.thy \ |
952 Tools/ComputeFloat.thy Tools/float_arith.ML \ |
952 Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy Tools/float_arith.ML \ |
953 Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy \ |
953 Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy \ |
954 Matrix/document/root.tex Matrix/ROOT.ML Matrix/cplex/Cplex.thy \ |
954 Matrix/document/root.tex Matrix/ROOT.ML Matrix/cplex/Cplex.thy \ |
955 Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML \ |
955 Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML \ |
956 Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \ |
956 Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \ |
957 Matrix/cplex/matrixlp.ML |
957 Matrix/cplex/matrixlp.ML |