src/HOL/Matrix/SparseMatrix.thy
changeset 15678 28cc2314c7ff
parent 15580 900291ee0af8
child 16041 5a8736668ced