src/HOL/Library/FrechetDeriv.thy
changeset 33820 082d9bc6992d
parent 32960 69916a850301
child 34146 14595e0c27e8