src/HOL/Analysis/Path_Connected.thy
changeset 79010 aceca8baf804
parent 78698 1b9388e6eb75
child 80052 35b2143aeec6