src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 58476 6ade4c7109a8
parent 57865 dcfb33c26f50
child 58776 95e58e04e534