src/HOL/Matrix/cplex/MatrixLP.thy
changeset 23174 3913451b0418
parent 20782 18abee32d1b6
child 23665 825bea0266db
equal deleted inserted replaced
23173:51179ca0c429 23174:3913451b0418
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Steven Obua
     3     Author:     Steven Obua
     4 *)
     4 *)
     5 
     5 
     6 theory MatrixLP 
     6 theory MatrixLP 
     7 imports Cplex
     7 imports Cplex "~~/src/Tools/Compute_Oracle/Compute_Oracle"
     8 uses ("matrixlp.ML")
     8 uses ("matrixlp.ML")
     9 begin
     9 begin
    10 
    10 
    11 constdefs
    11 constdefs
    12   list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
    12   list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"