src/HOL/Matrix/MatrixGeneral.thy
changeset 19710 ee9c7fa80d21
parent 16933 91ded127f5f7
child 20217 25b068a99d2b