src/HOL/Vector_Spaces.thy
changeset 78888 95bbf9a576b3
parent 73932 fd21b4a93043
child 80932 261cd8722677
equal deleted inserted replaced
78886:b82c2f801f2c 78888:95bbf9a576b3