src/HOL/Matrix/SparseMatrix.thy
changeset 22781 18fbba942a80
parent 22452 8a86fd2a1bf0
child 23477 f4b83f03cac9