Changes

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;
19. check that Isar proofs contain one 'show'
20. include unnamed chained facts in Sledgehammer's relevance filter
21. merge
22. removed hack in Sledgehammer that confuses preplay and gives Sledgehammer a strange semantics
23. don't freeze terms in Sledgehammer, as this has a bad impact on 'using' facts
24. tuned T functions: now 0 if not recursive
25. minor performance tuning;
26. tuned;
27. more zproofs; clarified signature;
28. misc tuning and clarification; eliminate clones (see also 3ae09d27ee7a);
29. more zproofs;
30. more operations;
31. more operations;
32. tuned;
33. clarified signature;
34. more zproofs;
35. more ML pretty-printing;
36. clarified const_proof vs. zproof_name;