src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 69448 51e696887b81
parent 69260 0a9688695a1b
child 69508 2a4c8a2a3f8e