src/HOL/Analysis/Smooth_Paths.thy
changeset 82276 d22e9c5b5dc6
parent 80052 35b2143aeec6