src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 68743 91162dd89571
parent 68607 67bb59e49834
child 69064 5840724b1d71