src/HOL/Matrix/SparseMatrix.thy
changeset 27685 cd561f58076d
parent 27653 180e28bab764
child 28562 4e74209f113e