src/HOL/Analysis/Linear_Algebra.thy
changeset 69608 2b3a247889f8
parent 69600 86e8e7347ac0
child 69619 3f7d8e05e0f2