src/HOL/Real_Vector_Spaces.thy
changeset 66744 fec1504e5f03
parent 66422 2891f33ed4c8
child 66793 deabce3ccf1f
equal deleted inserted replaced
66743:ff05d922bc34 66744:fec1504e5f03