HOL-Complex-Matrix: fixed deps;
authorwenzelm
Wed, 21 Sep 2005 11:50:20 +0200
changeset 17546 07371b92d382
parent 17545 1ba448f96af1
child 17547 b0d70cf4ed18
HOL-Complex-Matrix: fixed deps;
src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Sep 21 11:49:31 2005 +0200
+++ b/src/HOL/IsaMakefile	Wed Sep 21 11:50:20 2005 +0200
@@ -6,7 +6,7 @@
 
 default: HOL
 generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
-images: HOL HOL-Algebra HOL-Complex TLA HOL4
+images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix TLA HOL4
 
 #Note: keep targets sorted (except for HOL-Library)
 test: \
@@ -16,7 +16,6 @@
   HOL-Bali \
   HOL-Complex-ex \
   HOL-Complex-Import \
-  HOL-Complex-Matrix \
   HOL-Extraction \
       HOL-Complex-HahnBanach \
   HOL-Hoare \
@@ -640,7 +639,7 @@
 
 ## HOL-Complex-Matrix
 
-HOL-Complex-Matrix: HOL $(OUT)/HOL-Complex-Matrix
+HOL-Complex-Matrix: HOL-Complex $(OUT)/HOL-Complex-Matrix
 
 $(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
   Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \