src/HOL/Matrix/MatrixGeneral.thy
changeset 25345 dd5b851f8ef0
parent 23373 ead82c82da9e
child 25502 9200b36280c0