src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 67405 e9ab4ad7bd15
parent 67399 eab6ce8368fa
child 67613 ce654b0e6d69