Changes

Summary

1. two new induction principles on multisets
2. merged
3. clarified session imports;
4. clarified standard_import: based on Known.get_file as in PIDE editors;
5. afford unconditional all_known = true (reverting ea42dfd95ec8), for practical usability of qualified imports from arbitrary sessions;
6. proper imports_resources for import_name: avoid self-referential name resolution;
7. more precise position information;
8. tuned imports;
9. proper "~~" backup as documented;
10. clarified: explicit check of result;
11. clarified imports;
12. clarified local_theories: exclude ancestor sessions;
13. more standard master_dir;
14. eliminated default_qualifier: just a constant;
15. more uniform isabelle_scala; more uniform ISABELLE_SCALAC_OPTIONS with heap options;
16. include imports that morally belong to Main and are used in HOL-Proofs applications;
17. tuned;
18. proper theory_qualifier;
19. more global theories;
20. actual update_imports operations;
21. more operations;
22. tuned signature;
23. more operations;
24. tuned signature;
25. tuned whitespace;
26. clarified;
27. store Sessions.Info.name;
28. wrapper for "isabelle update_imports" with selection options like "isabelle build";
29. more position information;