minor performance tuning;

tuned;

more thorough treatment of hidden type variables within zproof;

more uniform treatment of "hyps" within zproof;

clarified order: follow Thm.fold_terms;

merged

clarified signature;

clarified signature;

tuned signature;

tuned;

clarified test: no exception yet;

tuned;

tuned;

tuned signature: more direct operations;

clarified signature;

clarified signature: more direct operations;

tuned signature;

tuned;

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;