clarified signature;

proper output of raw ML;

theory qualifier is always session name (see also 31e8a86971a8);

clarified session structure;

discontinued somewhat pointless session group: -g ZF may be replaced by -D ~~/src/ZF;

merged

clarified empty merge; tuned;

permissive loaded_theories (amending 67dbf5cdc056): user errors are produced e.g. in Known.make;

prefer native platform x86-windows, to make this work on x86_64-cygwin;

tuned signature;

even more robust syntax (amending 122df1fde073);

clarified error for bad session-qualified imports;

clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;

merged

completion supports theory header imports; tuned;

clarified modules;

tuned signature;

new theorem at_within_cbox_finite

process ROOT files only once, which allows duplicate (or overlapping) session root directories;

prefer Cygwin64, although some components still require update;

updated test version;

more recent polyml-test version;

misc tuning and modernization;

discontinued obsolete 'files' in session ROOT;

prefer file dependencies wrt. specific theories;

added command 'external_file';

proper document (cf. 9f5bfef8bd82);

removed pointless dependencies: done by 'spark_open';

merged

more documentation;