Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

1. tuned: less redundant implementation;
2. clarified signature: copy directory content more directly;
3. more robust;
4. tuned whitespace;
5. clarified signature: more general operations;
6. clarified signature;
7. tuned signature;