src/HOL/Matrix/Matrix.thy
changeset 33556 cba22e2999d5
parent 32960 69916a850301
child 33657 a4179bf442d1