src/HOL/Matrix/MatrixGeneral.thy
changeset 23279 e39dd93161d9
parent 22458 bd4379c9b4d0
child 23315 df3a7e9ebadb