src/HOL/IsaMakefile
changeset 32491 d5d8bea0cd94
parent 32478 521cc9bf2958
child 32500 7106aeb6dd64
     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	\