src/HOL/Analysis/Line_Segment.thy
changeset 73740 c46ff0efa1ce
parent 72569 d56e4eeae967
child 73932 fd21b4a93043