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