src/HOL/Library/FrechetDeriv.thy
changeset 30627 fb9e73c01603
parent 30273 ecd6f0ca62ea
child 30663 0b6aff7451b2