src/HOL/Matrix/SparseMatrix.thy
changeset 23579 1a8ca0e480cd
parent 23477 f4b83f03cac9
child 24124 4399175e3014