src/HOL/Matrix/Matrix.thy
changeset 31106 9a1178204dc0
parent 29700 22faf21db3df
child 32440 153965be0f4b