Added new functions to handle HOL goals and lemmas.
Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file.
Removed several functions definitions, and combined them with those in other files.
(* Title: HOL/Matrix/cplex/Cplex.thy
ID: $Id$
Author: Steven Obua
*)
theory Cplex
imports FloatSparseMatrix
uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML"
begin
end