src/HOL/Matrix/SparseMatrix.thy
changeset 15911 b730b0edc085
parent 15580 900291ee0af8
child 16041 5a8736668ced