src/HOL/Matrix/ROOT.ML

theorem(_i): empty target;
forget_proof: removed tmp hack;

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

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