src/HOL/Analysis/Line_Segment.thy
changeset 81144 6e6766cddf73
parent 79582 7822b55b26ce