src/HOL/Library/FrechetDeriv.thy
changeset 37511 26afa11a1fb2
parent 36626 72d2cb5c3db9
child 37729 daea77769276