src/HOL/Matrix/Matrix.thy
changeset 17215 8b969275a5d2
parent 16733 236dfafbeb63
child 17915 e38947f9ba5e