diff -r 1ba448f96af1 -r 07371b92d382 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 \