src/HOL/Analysis/Convex.thy
changeset 79021 1c91e884035d
parent 78656 4da1e18a9633
child 79532 bb5d036f3523