src/HOL/Matrix/Matrix.thy
changeset 38348 cf7b2121ad9d
parent 38273 d31a34569542
child 38526 a9ce311eb6b9