src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 72087 43a43b182a81
parent 71938 e1b262e7480c
child 72356 5a8c93a5ab4f