more direct proofs for type classes; misc tuning and cleanup;

tuned;

clarified modules: inference kernel maintains sort algebra within the logic;

more elementary treatment of standard_vars (unconstrainT is already standard);

clarified module structure;

simplified module structure: back to plain datatype (see 95f4f08f950f and 70019ab5e57f);

abstract type theory_id -- ensure non-equality type independently of implementation;

clarified export: retain proof boxes as local definitions -- more scalable;

reduced dependencies

clarified global theory context;

more robust export, based on reconstruct_proof / expand_proof;

clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;

tuned -- fewer warnings;

discontinued pointless messages;

clarified context;

clarified modules;

discontinue clean_proof: without type args its PThm nodes are not expanded, but with type args it is too unstable;

merged

more diagnostic operations;

tuned -- non-strict args;

proper constrains_map -- for shyps that are covered by present variables (amending 251f1fb44ccd);

tuned signature;

clarified signature; tuned;

tuned signature;

News for bind infixl

Monadic bind is now infixl as is the norm

purge remains from test (cf. 5a53724fe247);

tuned;

clarified signature;

removed obsolete RC tags;