src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 48003 1d11af40b106
parent 47445 69e96e5500df
child 49529 d523702bdae7