src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 71035 6fe5a0e1fa8e
parent 71028 c2465b429e6e
child 71030 b6e69c71a9f6