src/HOL/Analysis/Line_Segment.thy
changeset 73798 1ca35197108f
parent 72569 d56e4eeae967
child 73932 fd21b4a93043