src/HOL/Real_Vector_Spaces.thy
changeset 68724 7fafadbf16c7
parent 68721 53ad5c01be3f
child 69064 5840724b1d71