src/HOL/Matrix/ROOT.ML

export: simultaneous facts, refer to Variable.export;
Term.internal/skolem;

(*  Title:      HOL/Matrix/ROOT.ML
    ID:         $Id$
*)

use_thy "SparseMatrix";
with_path "cplex" use_thy "MatrixLP";