src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 73282 dcadb3243cfa
parent 72356 5a8c93a5ab4f
child 73795 8893e0ed263a