src/HOL/Matrix/MatrixGeneral.thy
changeset 23024 70435ffe077d
parent 22458 bd4379c9b4d0
child 23315 df3a7e9ebadb