src/HOL/Library/FrechetDeriv.thy
changeset 30747 b8ca7e450de3
parent 30729 461ee3e49ad3
child 31021 53642251a04f