src/HOL/RealVector.thy
changeset 36424 f3f389fc7974
parent 36409 d323e7773aa8
child 36795 e05e1283c550