Changes

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

Summary

1. tuned structure;
2. tuned;
3. merged
4. performance tuning: cache for ztyp_of within zterm_of; clarified signature;
5. tuned names;
6. minor performance tuning;
7. more zproofs;
8. minor performance tuning;
9. tuned;
10. more zproofs;
11. clarified modules;
12. more zproofs;
13. more zproofs;
14. proper treatment of ZConstP: term represents body of closure;
15. proper substitution of types within term;
16. more accurate treatment of term variables after instantiation of type variables;
17. tuned signature;
18. tuned;