tuned: more antiquotations;

tuned: more antiquotations;

tuned: more antiquotations;

tuned proofs;

tuned signature: more operations;

tuned;

tuned: more antiquotations;

clarified signature;

Two little lemmas

merged

more uniform Type_Infer_Context.infer_types_finished, despite subtle differences of Type_Infer.fixate vs. Proof_Context.standard_term_check_finish;

tuned, following cdae621613da;

tuned;

more robust: only type inference with its finish/fixate phase (on contrast to dc387e3999ec), e.g. avoid accidental "improvement" of type class operations (free vs. const);

tuned: more antiquotations;

tuned: more abstract access to datatype typ;

tuned (see also db120661dded);

tuned: more antiquotations;

tuned signature: eliminate aliases;

removed odd clone (amending 100c0eaf63d5); NB: Case_Translation.make_tnames covers TVar case as well, but this is not relevant here;

clarified: more robust (dest_Type_name o body_type), which may fail in both parts;

tuned: more antiquotations, more abstract access to datatype typ;

recover lost update (see 11b8f2e4c3d2 and 4041e7c8059d);

prefer host that is less likely to be down;

tuned: more antiquotations, avoid re-certification;

Rearranged a couple of theorems

New library material; also fixed the spelling error powr_ge_pzero -> powr_ge_zero

merged