support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;

clarified signature: proper typargs;

merged

export locale content; read_theory_names: proper classrel, arities; tuned signature;

tuned;

Some basic materials on filters and topology

merged

more accurate position for auxiliary files;

clarified signature;

tuned;

more careful treatment position: existing facts refer to interpretation command, future facts refer to themselves (see also 4270da306442);

tuned;

tuned signature;

clarified signature;

clarified signature: explicit type Locale.registration;

tuned;

tuned;

updated URL to remote TPTP, following heads-up from Geoff Sutcliffe

prefer "locale begin ... end";

tuned signature;

support Thy_Element in Scala, following ML version;

tuned;

tuned;

tuned;