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