src/HOL/Matrix/Matrix.thy
changeset 36726 47ba1770da8e
parent 35818 680caf709510
child 37765 26bdfb7b680b