src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 78517 28c1f4f5335f
parent 78516 56a408fa2440
child 79582 7822b55b26ce