src/HOL/Matrix/cplex/ROOT.ML
changeset 16873 9ed940a1bebb
parent 16792 e6ba3819e404
equal deleted inserted replaced
16872:a51699621d22 16873:9ed940a1bebb
     1 (*  Title:      HOL/Matrix/cplex/ROOT.ML
     1 (*  Title:      HOL/Matrix/cplex/ROOT.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3 *)
     3 *)
     4 
     4 
     5 (*use_thy "Cplex";*)
     5 use_thy "MatrixLP";