src/HOL/Real_Vector_Spaces.thy
changeset 67084 e138d96ed083
parent 66793 deabce3ccf1f
child 67135 1a94352812f4
equal deleted inserted replaced
67083:6b2c0681ef28 67084:e138d96ed083