isabelle: src/HOL/Matrix/cplex/Cplex.thy@3045683749af (annotated)

16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	1	(* Title: HOL/Matrix/cplex/Cplex.thy
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	2	ID: $Id$
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	3	Author: Steven Obua
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	4	*)
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	5
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	6	theory Cplex
23665 825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning obua parents: 16890 diff changeset	7	imports FloatSparseMatrix "~~/src/HOL/Tools/ComputeNumeral"
16890 c4e5afaba440 isatool fixheaders; wenzelm parents: 16784 diff changeset	8	uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML"
16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	9	begin
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	10
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	11	end
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	12
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	13
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	14