equal
deleted
inserted
replaced
1 (* Title: HOL/Matrix/FloatSparseMatrixBuilder.ML |
1 (* Title: HOL/Matrix_LP/FloatSparseMatrixBuilder.ML |
2 Author: Steven Obua |
2 Author: Steven Obua |
3 *) |
3 *) |
4 |
4 |
5 signature FLOAT_SPARSE_MATRIX_BUILDER = |
5 signature FLOAT_SPARSE_MATRIX_BUILDER = |
6 sig |
6 sig |