src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 79346 f86c310327df
parent 78516 56a408fa2440
child 79582 7822b55b26ce