src/HOL/RealVector.thy
changeset 29427 7ba952481e29
parent 29252 ea97aa6aeba2
child 29608 564ea783ace8