src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 68681 14167c321d22
parent 68607 67bb59e49834
child 69064 5840724b1d71