src/HOL/Matrix/Matrix.thy
changeset 17919 09adb77ac16c
parent 17915 e38947f9ba5e
child 20633 e98f59806244