Changes

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

Summary

1. merged
2. misc tuning and clarification;
3. tuned signature;
4. tuned;
5. tuned --- Token.make_string / Token.assign are value-oriented;
6. more documentation;
7. tuned signature;
8. tuned signature;
9. more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);
10. prefer static simpset;
11. omit pointless morphism in global theory;
12. more operations;
13. more careful treatment of context for method source;
14. clarified context;
15. clarified signature;
16. remove pointless context setup (see also b2e449c155a4);
17. more careful reset_context for stored entity;
18. more careful reset/set_context for stored declarations;
19. tuned;
20. tuned;
21. clarified signature: more explicit types;
22. clarified data: avoid pointless Morphism.transform;
23. proper Token.Declaration for internal_declaration;
24. more standard treatment of morphism context;
25. tuned: avoid duplication;
26. more standard treatment of morphism context, but hardly relevant here;
27. tuned;
28. more careful treatment of set_context / reset_context for persistent morphisms; avoid persistent theory for eq_morphism / eq_term_morphism, notably in 'class' definition;
29. clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context; clarified signature;
30. tuned signature;
31. support for context within morphism (for background theory);
32. proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs";
33. clarified signature;
34. tuned;
35. tuned;
36. tuned signature;
37. more accurate Thm.trim_context / Thm.transfer;
38. clarified stored thm: result from notes; tuned;
39. tuned whitespace;
40. clarified signature: avoid convoluted operations;
41. tuned signature;
42. update to polyml-a5d5fba90286, with more robust ML_Heap.sizeof;
43. avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c);
44. proper transfer / trim_context;
45. more operations "without_context", assuming that the thm has been properly transferred already;
46. proper trim_context / transfer;
47. tuned: more accurate check (is_norm_hhf protect);
48. clarified build options: reduce heap size by approx. 3%;
49. more standard merge order, following logical structure of imports rather than physical serials;
50. tuned;
51. tuned;
52. proper Thm.trim_context / Thm.transfer;
53. proper Thm.trim_context / Thm.transfer;
54. tuned: avoid pointless Proof_Context.init_global of Context.proof_of;