src/HOL/Matrix/SparseMatrix.thy
changeset 25345 dd5b851f8ef0
parent 25303 0699e20feabd
child 26300 03def556e26e