src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 78127 24b70433c2e8
parent 77935 7f240b0dabd9
child 78516 56a408fa2440
equal deleted inserted replaced
78122:f3d19c8445ec 78127:24b70433c2e8