--- a/src/HOL/IsaMakefile Tue Jun 21 08:16:03 2005 +0200
+++ b/src/HOL/IsaMakefile Tue Jun 21 09:31:57 2005 +0200
@@ -16,6 +16,7 @@
HOL-Bali \
HOL-Complex-ex \
HOL-Complex-Import \
+ HOL-Complex-Matrix \
HOL-Extraction \
HOL-Complex-HahnBanach \
HOL-Hoare \
@@ -27,7 +28,6 @@
HOL-Isar_examples \
HOL-Lambda \
HOL-Lattice \
- HOL-Matrix \
HOL-MicroJava \
HOL-Modelcheck \
HOL-NanoJava \
@@ -620,11 +620,11 @@
@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
-## HOL-Matrix
+## HOL-Complex-Matrix
-HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
+HOL-Complex-Matrix: HOL $(LOG)/HOL-Complex-Matrix.gz
-$(LOG)/HOL-Matrix.gz: $(OUT)/HOL-Complex \
+$(LOG)/HOL-Complex-Matrix.gz: $(OUT)/HOL-Complex \
Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
Matrix/document/root.tex Matrix/ROOT.ML
@$(ISATOOL) usedir $(OUT)/HOL-Complex Matrix
@@ -690,7 +690,7 @@
$(LOG)/HOL-Bali.gz \
$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
- $(LOG)/HOL-Lattice $(LOG)/HOL-Matrix \
+ $(LOG)/HOL-Lattice $(LOG)/HOL-Complex-Matrix \
$(LOG)/HOL-Complex.gz \
$(LOG)/HOL-Complex-ex.gz \
$(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \