changeset 24135 | e7fb7ef2a85e |
parent 23665 | 825bea0266db |
child 24302 | 3045683749af |
--- a/src/HOL/Matrix/cplex/fspmlp.ML Thu Aug 02 22:16:49 2007 +0200 +++ b/src/HOL/Matrix/cplex/fspmlp.ML Thu Aug 02 22:43:47 2007 +0200 @@ -41,7 +41,7 @@ datatype bound_type = LOWER | UPPER -fun intbound_ord ((i1, b1),(i2,b2)) = +fun intbound_ord ((i1: int, b1),(i2,b2)) = if i1 < i2 then LESS else if i1 = i2 then (if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)