src/HOL/Analysis/Line_Segment.thy
changeset 80760 be8c0e039a5e
parent 79582 7822b55b26ce