Changes

Summary

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