src/HOL/IsaMakefile
changeset 32500 7106aeb6dd64
parent 32496 4ab00a2642c3
parent 32491 d5d8bea0cd94
child 32518 e3c4e337196c
--- a/src/HOL/IsaMakefile	Wed Sep 02 21:33:16 2009 +0200
+++ b/src/HOL/IsaMakefile	Wed Sep 02 21:34:13 2009 +0200
@@ -941,7 +941,7 @@
 
 HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
 
-$(LOG)/HOL-Matrix.gz: $(OUT)/HOL				\
+$(LOG)/HOL-Matrix.gz: $(OUT)/HOL					\
   $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy			\
   $(SRC)/Tools/Compute_Oracle/am_compiler.ML				\
   $(SRC)/Tools/Compute_Oracle/am_interpreter.ML				\
@@ -949,8 +949,8 @@
   $(SRC)/Tools/Compute_Oracle/linker.ML					\
   $(SRC)/Tools/Compute_Oracle/am_ghc.ML					\
   $(SRC)/Tools/Compute_Oracle/am_sml.ML					\
-  $(SRC)/Tools/Compute_Oracle/compute.ML	\
-  Tools/ComputeFloat.thy Tools/float_arith.ML \
+  $(SRC)/Tools/Compute_Oracle/compute.ML Matrix/ComputeFloat.thy	\
+  Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy Tools/float_arith.ML	\
   Matrix/Matrix.thy Matrix/SparseMatrix.thy Matrix/LP.thy		\
   Matrix/document/root.tex Matrix/ROOT.ML Matrix/cplex/Cplex.thy	\
   Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML	\