src/HOL/Real_Vector_Spaces.thy
changeset 61095 50e793295ce1
parent 61070 b72a990adfe2
child 61169 4de9ff3ea29a
equal deleted inserted replaced
61094:3d88cd531abe 61095:50e793295ce1