# HG changeset patch
# User wenzelm
# Date 1159562817 -7200
# Node ID 18abee32d1b6f152adcc4bcc063e5633258bc58c
# Parent  e26fe5c63c2f4f81cd8ee3cdd714c2737f287311
proper use of matrixlp.ML;

diff -r e26fe5c63c2f -r 18abee32d1b6 src/HOL/Matrix/cplex/MatrixLP.thy
--- 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
-