src/HOL/Vector_Spaces.thy
changeset 69232 2b913054a9cf
parent 69064 5840724b1d71
child 69593 3dda49e08b9d