src/HOL/Matrix/Matrix.thy
changeset 20192 956cd30ef3be
parent 17915 e38947f9ba5e
child 20633 e98f59806244