src/HOL/Real_Vector_Spaces.thy
changeset 66926 4cf560a6dd84
parent 66793 deabce3ccf1f
child 67135 1a94352812f4