src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 73718 ecb31c3bf980
parent 72356 5a8c93a5ab4f
child 73795 8893e0ed263a