src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 58839 ccda99401bc8
parent 58776 95e58e04e534
child 58877 262572d90bc6