src/HOL/Real_Vector_Spaces.thy
changeset 65672 3848e278c278
parent 65583 8d53b3bebab4
child 65680 378a2f11bec9