src/HOL/Matrix/cplex/fspmlp.ML
changeset 31971 8c1b845ed105
parent 24630 351a308ab58d
child 32960 69916a850301
     1.1 --- a/src/HOL/Matrix/cplex/fspmlp.ML	Thu Jul 09 17:34:59 2009 +0200
     1.2 +++ b/src/HOL/Matrix/cplex/fspmlp.ML	Thu Jul 09 22:01:41 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Matrix/cplex/fspmlp.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Steven Obua
     1.7  *)
     1.8  
     1.9 @@ -45,9 +44,9 @@
    1.10          (if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)
    1.11      else GREATER
    1.12  
    1.13 -structure Inttab = TableFun(type key = int val ord = (rev_order o int_ord));
    1.14 +structure Inttab = Table(type key = int val ord = (rev_order o int_ord));
    1.15  
    1.16 -structure VarGraph = TableFun(type key = int*bound_type val ord = intbound_ord);
    1.17 +structure VarGraph = Table(type key = int*bound_type val ord = intbound_ord);
    1.18  (* key -> (float option) * (int -> (float * (((float * float) * key) list)))) *)
    1.19  (* dest_key -> (sure_bound * (row_index -> (row_bound * (((coeff_lower * coeff_upper) * src_key) list)))) *)
    1.20