src/HOL/Library/FrechetDeriv.thy
changeset 44271 89f40a5939b2
parent 44127 7b57b9295d98
child 44282 f0de18b62d63