src/HOL/Real_Vector_Spaces.thy
changeset 66965 9cec50354099
parent 66793 deabce3ccf1f
child 67135 1a94352812f4