src/HOL/Hyperreal/FrechetDeriv.thy
changeset 26104 200b4e401e65
parent 23398 0b5a400c7595
child 27611 2c01c0bdb385