src/HOL/Matrix/Matrix.thy
changeset 44262 355d5438f5fb
parent 44174 d1d79f0e1ea6
child 45694 4a8743618257