src/HOL/Matrix/MatrixGeneral.thy
changeset 17401 9147c880ada6
parent 16933 91ded127f5f7
child 20217 25b068a99d2b
equal deleted inserted replaced
17400:6ede71a506f5 17401:9147c880ada6