src/HOL/Analysis/Linear_Algebra.thy
changeset 77210 1ffee8893b12
parent 76836 30182f9e1818
child 78127 24b70433c2e8