src/HOL/Real_Vector_Spaces.thy
changeset 56381 0556204bc230
parent 56369 2704ca85be98
child 56409 36489d77c484
equal deleted inserted replaced
56380:9bb2856cc845 56381:0556204bc230