src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 68259 80df7c90e315
parent 68074 8d50467f7555
child 68527 2f4e2aab190a