src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 56841 bc6faeadbf82
parent 56571 f4635657d66f
child 56889 48a745e1bde7