src/HOL/Matrix/Matrix.thy
changeset 37724 6607ccf77946
parent 35818 680caf709510
child 37765 26bdfb7b680b