src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 65337 27144776aefe
parent 65057 799bbbb3a395
child 65583 8d53b3bebab4