src/HOL/RealVector.thy
changeset 36634 f9b43d197d16
parent 36409 d323e7773aa8
child 36795 e05e1283c550