src/HOL/IsaMakefile
changeset 32500 7106aeb6dd64
parent 32496 4ab00a2642c3
parent 32491 d5d8bea0cd94
child 32518 e3c4e337196c
     1.1 --- a/src/HOL/IsaMakefile	Wed Sep 02 21:33:16 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Sep 02 21:34:13 2009 +0200
     1.3 @@ -941,7 +941,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 @@ -949,8 +949,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	\