src/HOL/Real_Vector_Spaces.thy
changeset 65495 60d4fbed2b1f
parent 65036 ab7e11730ad8
child 65578 e4997c181cce
equal deleted inserted replaced
65494:88e6442c3150 65495:60d4fbed2b1f