1.1 --- a/src/HOL/IsaMakefile Wed Sep 02 14:11:45 2009 +0200
1.2 +++ b/src/HOL/IsaMakefile Wed Sep 02 16:25:44 2009 +0200
1.3 @@ -940,7 +940,7 @@
1.4
1.5 HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
1.6
1.7 -$(LOG)/HOL-Matrix.gz: $(OUT)/HOL \
1.8 +$(LOG)/HOL-Matrix.gz: $(OUT)/HOL \
1.9 $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \
1.10 $(SRC)/Tools/Compute_Oracle/am_compiler.ML \
1.11 $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \
1.12 @@ -948,8 +948,8 @@
1.13 $(SRC)/Tools/Compute_Oracle/linker.ML \
1.14 $(SRC)/Tools/Compute_Oracle/am_ghc.ML \
1.15 $(SRC)/Tools/Compute_Oracle/am_sml.ML \
1.16 - $(SRC)/Tools/Compute_Oracle/compute.ML \
1.17 - Tools/ComputeFloat.thy Tools/float_arith.ML \
1.18 + $(SRC)/Tools/Compute_Oracle/compute.ML Matrix/ComputeFloat.thy \
1.19 + Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy Tools/float_arith.ML \
1.20 Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy \
1.21 Matrix/document/root.tex Matrix/ROOT.ML Matrix/cplex/Cplex.thy \
1.22 Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML \