src/HOL/Vector_Spaces.thy
changeset 68940 25b431feb2e9
parent 68627 e371784becd9
child 69064 5840724b1d71