src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 78127 24b70433c2e8
parent 77935 7f240b0dabd9
child 78516 56a408fa2440