file system structure separating HOL4 and HOL Light concerns

distribution of compatibility theories

formal infrastructure for import sessions

dropped dead code

tuned whitespace

spurious set/pred correction

explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction

explicit locations for import_theory and setup_theory, for better user interface conformance

discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);

tuned;

tuned;

tuned;

canonical argument order for attribute application;

clarified terminology of raw protocol messages;

tuned;

tuned signature -- emphasize Isabelle_Process Input vs. Output;

explicit syslog_limit reduces danger of low-level message flooding; tuned;

retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided); tuned;

clarified scope of exception handlers;

relevant timing as in ML; more PIDE modules;

more fundamental pred-to-set conversions for range and domain by means of inductive_set

merged

tuned whitespace

tuned import