# HG changeset patch
# User obua
# Date 1127152149 -7200
# Node ID f70d62d5f9c8e7ca21017adb8e0e22bd290b39a2
# Parent  67376a311a2b84acf6913b64a09b6ce210fb9eab
Removed superfluous HOL/Matrix/cplex/ROOT.ML.

diff -r 67376a311a2b -r f70d62d5f9c8 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Sep 19 18:30:22 2005 +0200
+++ b/src/HOL/IsaMakefile	Mon Sep 19 19:49:09 2005 +0200
@@ -639,25 +639,12 @@
 
 ## HOL-Complex-Matrix
 
-#HOL-Complex-Matrix: HOL $(LOG)/HOL-Complex-Matrix.gz
-
-#$(LOG)/HOL-Complex-Matrix.gz: $(OUT)/HOL-Complex \
-#  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
-#  Matrix/document/root.tex Matrix/ROOT.ML \
-#  Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
-#  Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
-#  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
-#  Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
-#	@$(ISATOOL) usedir $(OUT)/HOL-Complex Matrix
-
-## HOL-Complex-Matrix
-
 HOL-Complex-Matrix: HOL $(OUT)/HOL-Complex-Matrix
 
 $(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
   Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
   Matrix/document/root.tex Matrix/ROOT.ML \
-  Matrix/cplex/ROOT.ML Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
+  Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
   Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
   Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
   Matrix/cplex/MatrixLP.thy Matrix/cplex/MatrixLP.ML
diff -r 67376a311a2b -r f70d62d5f9c8 src/HOL/Matrix/cplex/ROOT.ML
--- a/src/HOL/Matrix/cplex/ROOT.ML	Mon Sep 19 18:30:22 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-(*  Title:      HOL/Matrix/cplex/ROOT.ML
-    ID:         $Id$
-*)
-
-use_thy "MatrixLP";
\ No newline at end of file