src/HOL/Matrix/cplex/MatrixLP.thy
changeset 20782 18abee32d1b6
parent 16873 9ed940a1bebb
child 23174 3913451b0418
     1.1 --- a/src/HOL/Matrix/cplex/MatrixLP.thy	Fri Sep 29 11:32:58 2006 +0200
     1.2 +++ b/src/HOL/Matrix/cplex/MatrixLP.thy	Fri Sep 29 22:46:57 2006 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4  
     1.5  theory MatrixLP 
     1.6  imports Cplex
     1.7 +uses ("matrixlp.ML")
     1.8  begin
     1.9  
    1.10  constdefs
    1.11 @@ -62,5 +63,6 @@
    1.12  lemmas sorted_sp_simps = SparseMatrix.sorted_sp_simps
    1.13  lemmas fst_snd_conv = Product_Type.fst_conv Product_Type.snd_conv
    1.14  
    1.15 +use "matrixlp.ML"
    1.16 +
    1.17  end
    1.18 -