src/HOL/Library/FrechetDeriv.thy
changeset 33242 99577c7085c8
parent 32960 69916a850301
child 34146 14595e0c27e8