src/HOL/Real_Vector_Spaces.thy
changeset 67191 9ab34bb83a84
parent 67135 1a94352812f4
child 67399 eab6ce8368fa