src/HOL/Matrix/SparseMatrix.thy
changeset 35032 7efe662e41b4
parent 35028 108662d50512
child 35416 d8d7d1b785af