src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 69517 dc20f278e8f3
parent 69510 0f31dd2e540d
child 69518 bf88364c9e94