prefer named lemmas -- more compact proofterms;

clarified signature;
more careful treatment of implicit context;

misc tuning and clarification, notably wrt. flow of context;

tuned signature;

clarified: use existing Thm.dest_ctyp_fun (which is more strict);

isabelle update -u control_cartouches;

isabelle update -u control_cartouches;

tuned signature;

ran isabelle update_op on all sources

always expand equalities in the transfer relation in transfer_prover (cf. 0a7c97c76f46)

Type_Infer.object_logic controls improvement of type inference result;

refactoring

rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;

new methods for debugging transfer and transfer_prover

right parenthesization

tuned -- avoid slightly odd @{cpat};

tuned signature;
clarified context;

tuned signature;

prefer tactics with explicit context;

simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);

clarified context;

clarified context;

Thm.cterm_of and Thm.ctyp_of operate on local context;

clarified signature;

tuned signature -- prefer qualified names;

proper context;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

renamed "pairself" to "apply2", in accordance to @{apply 2};

tuned; store pred_simps

added pred_def, rel_eq_onp tuned

modernized setup;

make SML/NJ happier;

setup for Transfer and Lifting from BNF; tuned thm names

--HG--
rename : src/HOL/Tools/transfer.ML => src/HOL/Tools/Transfer/transfer.ML