src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 67963 9541f2c5ce8d
parent 67962 0acdcd8f4ba1
child 67968 a5ad4c015d1c