src/HOL/Real_Vector_Spaces.thy
changeset 66120 e03ff7e831cc
parent 66089 def95e0bc529
child 66420 bc0dab0e7b40