src/HOL/Real_Vector_Spaces.thy
changeset 66478 439296f00ab5
parent 66422 2891f33ed4c8
child 66793 deabce3ccf1f
equal deleted inserted replaced
66477:7dccaa6d419a 66478:439296f00ab5