src/HOL/Matrix/MatrixGeneral.thy
changeset 17740 fc385ce6187d
parent 16933 91ded127f5f7
child 20217 25b068a99d2b
equal deleted inserted replaced
17739:eddebb044a62 17740:fc385ce6187d