src/HOL/Library/Convex_Euclidean_Space.thy
changeset 31945 d5f186aa0bed
parent 31660 84912dff2d74
child 32456 341c83339aeb