src/HOL/Matrix/Matrix.thy
changeset 28491 c5420429a5aa
parent 27653 180e28bab764
child 28562 4e74209f113e