equal
deleted
inserted
replaced
1 (* Title: HOL/Matrix/ROOT.ML |
1 (* Title: HOL/Matrix/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 *) |
3 *) |
4 |
4 |
5 use_thy "SparseMatrix"; |
5 use_thy "SparseMatrix"; |
6 cd "cplex"; use_thy "MatrixLP"; cd ".."; |
6 with_path "cplex" use_thy "MatrixLP"; |
7 |
|
8 |
|