minor performance tuning, for important special case where consts are already expanded (e.g. re-certification within proof procedure);

tuned whitespace;

more robust: certify types uniformly (see also 62b75508eb66);

tuned;

clarified signature;

clarified signature: avoid redundant Term.maxidx_of_term;

proper check of result from Soft_Type_System.global_purge (amending b2bedb022a75);

misc tuning and clarification: prefer Same.operation;

clarified signature;

tuned names;

clarified signature;

tuned whitespace;

clarified modules; minor performance tuning;

clarified signature;

added and removed lemmas

proper SMTP session: set envelope sender address correctly;

update javamail component with current jakarta mail APIs and eclipse angus implementation;

tuned source structure;

clarified signature; minor performance tuning;

tuned;

minor performance tuning; eliminate clones;

minor performance tuning;

minor performance tuning;

minor performance tuning;

minor performance tuning;

minor performance tuning;

minor performance tuning;

tuned;

tuned signature;

tuned signature;

more zproofs, underlying Proofterm.unconstrain_thm_proof / Thm.unconstrainT;

omit syntactic of_class check, which is in conflict with sort constraints within the logic;

tuned;

minor performance tuning;

clarified signature; clarified modules;

misc tuning and clarification;

tuned signature;

tuned signature: canonical argument order;

tuned;

clarified datatype ztyp: omit special case that rarely occurs (thanks to ZClass and ZClassp);

clarified box_proof: use sort constraints within the logic;

more operations (see also 8368160d3c65);

proper support for complex types, not just type variables (amending 623789141e39);

proper instantiation for make_const_proof, notably change of types for term variables;

tuned names;

more operations;

clarified signature;

minor performance tuning: proper Same.operation;

minor performance tuning: proper Same.operation; clarified modules;

tuned signature;

minor performance tuning: proper Same.operation; clarified modules;

minor performance tuning: proper Same.operation;

tuned signature;

tuned;

pro-forma support for ZTerm.sorts_zproof;

tuned comments;