# HG changeset patch
# User wenzelm
# Date 1119298437 -7200
# Node ID eaf7bb77fed690f2d9ee935f71d9a71fc0041cef
# Parent  ace3c2b9535327b53947fbeaf2640549b7d847df
HOL-Matrix: plain session;

diff -r ace3c2b95353 -r eaf7bb77fed6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jun 20 22:13:56 2005 +0200
+++ b/src/HOL/IsaMakefile	Mon Jun 20 22:13:57 2005 +0200
@@ -622,12 +622,13 @@
 
 ## HOL-Matrix
 
-HOL-Matrix: HOL HOL-Complex $(LOG)/HOL-Matrix.gz
+HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
 
 $(LOG)/HOL-Matrix.gz: $(OUT)/HOL-Complex \
   Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
   Matrix/document/root.tex Matrix/ROOT.ML
-	@cd Matrix; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL-Matrix
+	@$(ISATOOL) usedir $(OUT)/HOL-Complex Matrix
+
 
 ## TLA
 
@@ -689,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-Lattice $(LOG)/HOL-Matrix \
 		$(LOG)/HOL-Complex.gz \
 		$(LOG)/HOL-Complex-ex.gz \
 		$(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \