src/HOL/Library/FrechetDeriv.thy
changeset 49890 89eff795f757
parent 44568 e6f291cb5810
child 49962 a8cc904a6820