src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 71030 b6e69c71a9f6
parent 71028 c2465b429e6e
parent 71029 934e0044e94b
child 71172 575b3a818de5