src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 72034 452073b64f28
parent 71938 e1b262e7480c
child 72356 5a8c93a5ab4f