src/HOL/Analysis/Line_Segment.thy
changeset 77703 0262155d2743
parent 77140 9a60c1759543
child 78477 37abfe400ae6
equal deleted inserted replaced
77702:b5fbe9837aee 77703:0262155d2743