src/HOL/Matrix/SparseMatrix.thy
changeset 16389 48832eba5b1e
parent 16041 5a8736668ced
child 16417 9bc16273c2d4