src/HOL/Hyperreal/FrechetDeriv.thy
changeset 23024 70435ffe077d
parent 22720 296813d7d306
child 23398 0b5a400c7595