src/HOL/Hyperreal/HDeriv.thy
changeset 23024 70435ffe077d
parent 22653 8e016bfdbf2f
child 23398 0b5a400c7595