--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Fri Aug 17 09:19:53 2007 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Fri Aug 17 09:20:45 2007 +0200
@@ -15,6 +15,7 @@
val approx_matrix : int -> (float -> float) -> matrix -> term * term
val mk_spvec_entry : integer -> float -> term
+ val mk_spvec_entry' : integer -> term -> term
val mk_spmat_entry : integer -> term -> term
val spvecT: typ
val spmatT: typ
@@ -64,6 +65,9 @@
fun mk_spvec_entry i f =
HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, FloatArith.mk_float f);
+fun mk_spvec_entry' i x =
+ HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, x);
+
fun mk_spmat_entry i e =
HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, e);