src/HOL/Matrix/cplex/Cplex.thy
author wenzelm
Thu, 08 Nov 2007 14:51:30 +0100
changeset 25345 dd5b851f8ef0
parent 23665 825bea0266db
child 27484 dbb9981c3d18
permissions -rw-r--r--
renamed ProofContext.read_const' to ProofContext.read_const_proper; export expand_abbrevs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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