src/HOL/Matrix/Matrix.thy
changeset 27710 29702aa892a5
parent 27653 180e28bab764
child 28562 4e74209f113e