src/HOL/Real_Vector_Spaces.thy
changeset 77208 a3f67a4459e1
parent 77138 c8597292cd41
child 77221 0cdb384bf56a
equal deleted inserted replaced
77207:d98a99e4eea9 77208:a3f67a4459e1