src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 82912 ad66fb23998a
parent 82802 547335b41005