src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 47884 21c42b095c84
parent 47445 69e96e5500df
child 49529 d523702bdae7