src/HOL/Real_Vector_Spaces.thy
changeset 64290 fb5c74a58796
parent 64272 f76b6dda2e56
child 64788 19f3d4af7a7d