src/HOL/Real_Vector_Spaces.thy
changeset 66548 253880668a43
parent 66422 2891f33ed4c8
child 66793 deabce3ccf1f
equal deleted inserted replaced
66547:188c7853f84a 66548:253880668a43