equal
deleted
inserted
replaced
1 (* Title: HOL/Matrix/cplex/CplexMatrixConverter.ML |
1 (* Title: HOL/Matrix/cplex/CplexMatrixConverter.ML |
2 ID: $Id$ |
|
3 Author: Steven Obua |
2 Author: Steven Obua |
4 *) |
3 *) |
5 |
4 |
6 signature MATRIX_BUILDER = |
5 signature MATRIX_BUILDER = |
7 sig |
6 sig |