# HG changeset patch
# User wenzelm
# Date 1119339117 -7200
# Node ID 20f4c6a950f7d93320dd130590be2ea42e2cafed
# Parent  5e5945ae284cfc1e2bafbf8d59987dedb051f8ae
fixed HOL-Complex-Matrix target;

diff -r 5e5945ae284c -r 20f4c6a950f7 src/HOL/IsaMakefile
--- 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 \