--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Jun 05 18:36:10 2007 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Tue Jun 05 19:19:30 2007 +0200
@@ -14,8 +14,8 @@
val approx_vector : int -> (float -> float) -> vector -> term * term
val approx_matrix : int -> (float -> float) -> matrix -> term * term
- val mk_spvec_entry : Intt.int -> float -> term
- val mk_spmat_entry : Intt.int -> term -> term
+ val mk_spvec_entry : integer -> float -> term
+ val mk_spmat_entry : integer -> term -> term
val spvecT: typ
val spmatT: typ
@@ -64,7 +64,7 @@
fun app (index, s) (lower, upper) =
let
val (flower, fupper) = approx_value prec pprt s
- val index = HOLogic.mk_number HOLogic.natT (Intt.int index)
+ val index = HOLogic.mk_number HOLogic.natT (Integer.int index)
val elower = HOLogic.mk_prod (index, flower)
val eupper = HOLogic.mk_prod (index, fupper)
in (elower :: lower, eupper :: upper) end;
@@ -77,7 +77,7 @@
fun app (index, v) (lower, upper) =
let
val (flower, fupper) = approx_vector prec pprt v
- val index = HOLogic.mk_number HOLogic.natT (Intt.int index)
+ val index = HOLogic.mk_number HOLogic.natT (Integer.int index)
val elower = HOLogic.mk_prod (index, flower)
val eupper = HOLogic.mk_prod (index, fupper)
in (elower :: lower, eupper :: upper) end;