uniform import_name, with treatment of global and qualified theories;

tuned signature;

more concise criterion

tuned

more on lists

store totality fact in function info

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;

macbroy30 is on 10.12 Sierra (already since 04-Mar-2017) -- discontinued support for 10.8 Mountain Lion;

back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";

tuned headers;

proper imports; tuned headers;

tuned message;

merged

misc tuning and modernization;

clarified imports;

tuned signature;