src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 79806 ba8fb71587ae
parent 79582 7822b55b26ce
child 82802 547335b41005
equal deleted inserted replaced
79804:1f7dcfdb3e67 79806:ba8fb71587ae