src/HOL/Matrix/Matrix.thy
changeset 39190 a2775776be3f
parent 38526 a9ce311eb6b9
child 39302 d7728f65b353