src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
changeset 47846 bbc3e7bccc61
parent 47445 69e96e5500df
child 49529 d523702bdae7