src/HOL/Library/FrechetDeriv.thy
changeset 30129 419116f1157a
parent 29986 6b1ccda8bf19
child 30273 ecd6f0ca62ea