src/HOL/Analysis/Line_Segment.thy
changeset 80402 b8c5b23ce24c
parent 79582 7822b55b26ce