src/HOL/Library/FrechetDeriv.thy
changeset 37380 35815ce9218a
parent 36626 72d2cb5c3db9
child 37729 daea77769276