--- a/src/HOL/IsaMakefile Fri Sep 03 10:27:05 2004 +0200
+++ b/src/HOL/IsaMakefile Fri Sep 03 17:10:36 2004 +0200
@@ -1,5 +1,3 @@
-#
-# $Id$
#
# IsaMakefile for HOL
#
@@ -80,8 +78,7 @@
$(SRC)/Provers/quasi.ML \
$(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
$(SRC)/Provers/trancl.ML \
- $(SRC)/TFL/isand.ML $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML\
- $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
+ $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
$(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
$(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
@@ -97,8 +94,7 @@
Nat.thy NatArith.ML NatArith.thy \
Power.thy PreList.thy Product_Type.ML Product_Type.thy \
Refute.thy ROOT.ML \
- Recdef.thy Reconstruction.thy Record.thy\
- Relation.ML Relation.thy Relation_Power.ML \
+ Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\
Set.ML Set.thy SetInterval.ML SetInterval.thy \
Sum_Type.ML Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
@@ -109,7 +105,7 @@
Tools/primrec_package.ML \
Tools/prop_logic.ML \
Tools/recdef_package.ML Tools/recfun_codegen.ML \
- Tools/record_package.ML Tools/reconstruction.ML\
+ Tools/record_package.ML \
Tools/refute.ML Tools/refute_isar.ML \
Tools/rewrite_hol_proof.ML \
Tools/sat_solver.ML \
@@ -635,14 +631,18 @@
## HOL-Matrix
-HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
+HOL-Matrix: HOL HOL-Complex $(LOG)/HOL-Matrix.gz
-$(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ROOT.ML \
- Matrix/Matrix.thy Matrix/LinProg.thy Matrix/MatrixGeneral.thy \
- Matrix/SparseMatrix.thy Matrix/document/root.tex
- @$(ISATOOL) usedir $(OUT)/HOL Matrix
-
-
+$(LOG)/HOL-Matrix.gz: $(OUT)/HOL-Complex \
+ Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
+ Matrix/Float.thy Matrix/FloatArith.ML Matrix/ExactFloatingPoint.ML \
+ Matrix/Cplex.ML Matrix/CplexMatrixConverter.ML \
+ Matrix/FloatSparseMatrixBuilder.ML \
+ Matrix/conv.ML Matrix/eq_codegen.ML Matrix/codegen_prep.ML \
+ Matrix/fspmlp.ML \
+ Matrix/MatrixLP_gensimp.ML Matrix/MatrixLP.ML Matrix/MatrixLP.thy \
+ Matrix/document/root.tex Matrix/ROOT.ML
+ @cd Matrix; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL-Matrix
## TLA