src/HOL/Matrix/cplex/CplexMatrixConverter.ML
changeset 16838 131ca99f6abf
parent 16784 92ff7c903585
child 17261 193b84a70ca4
equal deleted inserted replaced
16837:416e86088931 16838:131ca99f6abf
    46 		     
    46 		     
    47 open matrix_builder 
    47 open matrix_builder 
    48 open cplex
    48 open cplex
    49      
    49      
    50 exception Converter of string;
    50 exception Converter of string;
    51 
       
    52 structure Inttab = TableFun(type key = int val ord = int_ord);
       
    53 
    51 
    54 fun neg_term (cplexNeg t) = t
    52 fun neg_term (cplexNeg t) = t
    55   | neg_term (cplexSum ts) = cplexSum (map neg_term ts)
    53   | neg_term (cplexSum ts) = cplexSum (map neg_term ts)
    56   | neg_term t = cplexNeg t 
    54   | neg_term t = cplexNeg t 
    57 	      
    55