src/HOL/Real_Vector_Spaces.thy
changeset 73658 f6b453449cc6
parent 73411 1f1366966296
child 73932 fd21b4a93043