proper use of matrixlp.ML;

--- a/src/HOL/Matrix/cplex/MatrixLP.thy	Fri Sep 29 11:32:58 2006 +0200
+++ b/src/HOL/Matrix/cplex/MatrixLP.thy	Fri Sep 29 22:46:57 2006 +0200
@@ -5,6 +5,7 @@
 
 theory MatrixLP 
 imports Cplex
+uses ("matrixlp.ML")
 begin
 
 constdefs
@@ -62,5 +63,6 @@
 lemmas sorted_sp_simps = SparseMatrix.sorted_sp_simps
 lemmas fst_snd_conv = Product_Type.fst_conv Product_Type.snd_conv
 
+use "matrixlp.ML"
+
 end
-