src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 73880 9ce206f6e8c6
parent 73795 8893e0ed263a
child 77935 7f240b0dabd9
equal deleted inserted replaced
73879:0db0cd462163 73880:9ce206f6e8c6