src/HOL/Hyperreal/FrechetDeriv.thy
changeset 28145 af3923ed4786
parent 27611 2c01c0bdb385
child 28823 dcbef866c9e2