src/HOL/Real_Vector_Spaces.thy
changeset 69008 d55783ea6cf6
parent 68721 53ad5c01be3f
child 69064 5840724b1d71