src/HOL/Matrix/cplex/Cplex_tools.ML
changeset 17412 e26cb20ef0cc
parent 16966 37e34f315057
child 17521 0f1c48de39f5
equal deleted inserted replaced
17411:664434175578 17412:e26cb20ef0cc
   723   | bound2constr (cplexBound (t1, c1, t2)) = 
   723   | bound2constr (cplexBound (t1, c1, t2)) = 
   724     norm_Constr(cplexConstr (c1, (t1,t2)))
   724     norm_Constr(cplexConstr (c1, (t1,t2)))
   725 
   725 
   726 val emptyset = Symtab.empty
   726 val emptyset = Symtab.empty
   727 
   727 
   728 fun singleton v = Symtab.update ((v, ()), emptyset)
   728 fun singleton v = Symtab.update (v, ()) emptyset
   729 
   729 
   730 fun merge a b = Symtab.merge (op =) (a, b)
   730 fun merge a b = Symtab.merge (op =) (a, b)
   731 
   731 
   732 fun mergemap f ts = Library.foldl
   732 fun mergemap f ts = Library.foldl
   733 			(fn (table, x) => merge table (f x))
   733 			(fn (table, x) => merge table (f x))