1.1 --- a/src/HOL/IsaMakefile Sat Mar 17 12:26:19 2012 +0100
1.2 +++ b/src/HOL/IsaMakefile Sat Mar 17 12:52:40 2012 +0100
1.3 @@ -52,7 +52,7 @@
1.4 HOL-Isar_Examples \
1.5 HOL-Lattice \
1.6 HOL-Library-Codegenerator_Test \
1.7 - HOL-Matrix \
1.8 + HOL-Matrix_LP \
1.9 HOL-Metis_Examples \
1.10 HOL-MicroJava \
1.11 HOL-Mirabelle \
1.12 @@ -1172,22 +1172,26 @@
1.13 @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
1.14
1.15
1.16 -## HOL-Matrix
1.17 +## HOL-Matrix_LP
1.18
1.19 -HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
1.20 +HOL-Matrix_LP: HOL $(LOG)/HOL-Matrix_LP.gz
1.21
1.22 -$(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ComputeFloat.thy \
1.23 - Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy \
1.24 - Matrix/Compute_Oracle/Compute_Oracle.thy Matrix/Compute_Oracle/am.ML \
1.25 - Matrix/Compute_Oracle/am_compiler.ML Matrix/Compute_Oracle/am_ghc.ML \
1.26 - Matrix/Compute_Oracle/am_interpreter.ML \
1.27 - Matrix/Compute_Oracle/am_sml.ML Matrix/Compute_Oracle/compute.ML \
1.28 - Matrix/Compute_Oracle/linker.ML Matrix/Cplex.thy \
1.29 - Matrix/CplexMatrixConverter.ML Matrix/Cplex_tools.ML \
1.30 - Matrix/FloatSparseMatrixBuilder.ML Matrix/LP.thy Matrix/Matrix.thy \
1.31 - Matrix/ROOT.ML Matrix/SparseMatrix.thy Matrix/document/root.tex \
1.32 - Matrix/fspmlp.ML Matrix/matrixlp.ML Tools/float_arith.ML
1.33 - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix
1.34 +$(LOG)/HOL-Matrix_LP.gz: $(OUT)/HOL Matrix_LP/ComputeFloat.thy \
1.35 + Matrix_LP/ComputeHOL.thy Matrix_LP/ComputeNumeral.thy \
1.36 + Matrix_LP/Compute_Oracle/Compute_Oracle.thy \
1.37 + Matrix_LP/Compute_Oracle/am.ML \
1.38 + Matrix_LP/Compute_Oracle/am_compiler.ML \
1.39 + Matrix_LP/Compute_Oracle/am_ghc.ML \
1.40 + Matrix_LP/Compute_Oracle/am_interpreter.ML \
1.41 + Matrix_LP/Compute_Oracle/am_sml.ML \
1.42 + Matrix_LP/Compute_Oracle/compute.ML \
1.43 + Matrix_LP/Compute_Oracle/linker.ML Matrix_LP/Cplex.thy \
1.44 + Matrix_LP/CplexMatrixConverter.ML Matrix_LP/Cplex_tools.ML \
1.45 + Matrix_LP/FloatSparseMatrixBuilder.ML Matrix_LP/LP.thy \
1.46 + Matrix_LP/Matrix.thy Matrix_LP/ROOT.ML Matrix_LP/SparseMatrix.thy \
1.47 + Matrix_LP/document/root.tex Matrix_LP/fspmlp.ML \
1.48 + Matrix_LP/matrixlp.ML Tools/float_arith.ML
1.49 + @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix_LP
1.50
1.51
1.52 ## TLA
1.53 @@ -1901,9 +1905,9 @@
1.54 $(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz \
1.55 $(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz \
1.56 $(LOG)/HOL-Library-Codegenerator_Test.gz \
1.57 - $(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix \
1.58 - $(LOG)/HOL-Matrix.gz $(LOG)/HOL-Metis_Examples.gz \
1.59 - $(LOG)/HOL-MicroJava.gz $(LOG)/HOL-Mirabelle.gz \
1.60 + $(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix_LP.gz \
1.61 + $(LOG)/HOL-Metis_Examples.gz $(LOG)/HOL-MicroJava.gz \
1.62 + $(LOG)/HOL-Mirabelle.gz \
1.63 $(LOG)/HOL-Multivariate_Analysis.gz \
1.64 $(LOG)/HOL-Mutabelle.gz $(LOG)/HOL-NSA-Examples.gz \
1.65 $(LOG)/HOL-NSA.gz $(LOG)/HOL-NanoJava.gz \