src/HOL/Hyperreal/FrechetDeriv.thy
changeset 27183 0fc4c0f97a1b
parent 23398 0b5a400c7595
child 27611 2c01c0bdb385