Changes

Summary

1. tuned;
2. NEWS;
3. miscellaneous examples and experiments for Isabelle/Pure;
4. tuned comments;
5. unused;
6. clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference);
7. NEWS;
8. clarified signature: more scalable operations;
9. more scalable operations;
10. more scalable operations;
11. clarified order of extra type variables, following names more often than occurrences;
12. clarified signature; tuned;
13. tuned;
14. more scalable operations;
15. omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused;
16. clarified signature;
17. more robust: client could have terminated already;
18. clarified signature;
19. clarified signature;
20. clarified modules;
21. clarified set of items with order of addition;
22. tuned message;
23. tuned whitespace;
24. clarified signature; clarified modules;
25. tuned;
26. simplified: uniqueness check happens in export_consumer;
27. more markup, e.g. to locate defining theory node in formal document output;
28. tuned signature;
29. export other entities, e.g. relevant for formal document output; clarified markup kind (PIDE) vs. export kind (e.g. MMT);
30. pointer_eq_ord: minor performance tuning;
31. more robust: progress.stopped means that build has failed;
32. more reactive interrupt;
33. more reactive interrupt;
34. more robust: retain length of results;
35. more reactive interrupt;
36. tuned signature;
37. tuned signature;
38. tuned signature;
39. tuned;
40. merged
41. clarified modules;
42. more scalable operations;
43. more scalable operations;
44. tuned;
45. clarified modules;
46. clarified signature; minor performance tuning;
47. more scalable operations;
48. unused;
49. more efficient operations: traverse hyps only when required;
50. more robust signature: result has no particular order;
51. more scalable operations;
52. unused;
53. more scalable operations;
54. clarified;
55. tuned signature;
56. clarified signature;
57. more scalable operations;
58. clarified signature;
59. tuned signature;
60. more scalable operations;
61. more scalable operations;
62. more scalable operations; tuned;
63. more scalable operations;
64. white space
65. merged
66. some fixes connected with card_Diff_singleton
67. strengthened a few lemmas about finite sets and added a code equation for complex_of_real
68. tuned;
69. proper inst table;
70. more scalable data structure (but: rarely used many arguments);
71. minor performance tuning: fewer allocations; clarified theory context;

Summary

1. eliminated Specification.definition', following Isabelle/6876e3d5e362;
2. clarified signature: more scalable operations, according to Isabelle/c2ee8d993d6a;
3. clarified signature, according to Isabelle/612b7e0d6721;
4. tuned signature, according to Isabelle/839a6e284545;
5. merged
6. Backed out changeset ef19e4e58b8c restoring old argument order on synthesized formulas
7. avoid hardwired document;
8. merged
9. tuned signature, according to Isabelle/9d9e7ed01dbb;
10. clarified signature, according to Isabelle/9d9e7ed01dbb;
11. clarified signature, according to Isabelle/9d9e7ed01dbb;
12. clarified signature, according to Isabelle/9d9e7ed01dbb;
13. simplified, using Isabelle/ML operations;
14. adapted to Isabelle/36774e8af3db: cannot rely on order of instantiation for vars;
15. tuned whitespace;
16. more scalable operations;
17. merged
18. synthesized formulas have their variables permuted
19. merged
20. fixes for cardinality lemmas
21. proper inst table;