Changes

Summary

1. allow to load this into "isabelle jedit -l HOL";
2. print like syntax of Thy_Header.header;
3. more explicit types;
4. proper name according to meaning;
5. more main sessions and global theories;
6. eliminated redundant imports;
7. eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;
8. tuned (see also 1fa1023b13b9);
9. tuned header;
10. tuned signature;
11. proper base name;
12. tuned;
13. tuned syntax; some official documentation;
14. clarified: allow to qualify theories from ROOT;
15. refer to global_theories from all sessions, before selection;
16. tuned signature;
17. tuned;