Changes

Summary

1. tuned: concise combinators instead of bulky case-expressions;
2. provide ML antiquotation "if_none": non-strict version of "the_default";
3. merged
4. proper Thm.trim_context / Thm.transfer (see also 0d401f874942);
5. tuned;
6. more operations;
7. more operations;
8. more uniform operations wrt. Thm.full_prop_of;
9. proper Thm.trim_context / Thm.transfer for context data;
10. tuned: more concise data record;
11. tuned;
12. clarified counters and types;
13. tuned signature;
14. support n-ary merge theory data; less redundant use of ids and stages;
15. tuned;
16. tuned;
17. proper theory_long_name;
18. prefer theory_long_name in data;
19. proper theory_long_name;
20. clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
21. tuned;
22. more operations, following Isabelle/ML conventions;
23. clarified theory_id: plain value without state;