prefer control symbol antiquotations;

Tuned generation of elimination rules in function package

more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;

tuned;

misc tuning and simplification;

tuned;

clarified context;

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

clarified context;

tuned signature -- prefer qualified names;

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

Fixed variable naming bug in function package

proper context for assume_tac (atac remains as fall-back without context);

tuning

tuned -- prefer canonical argument order of fold_rev;

proper simplifier context;
more standard "cert";

tuned;

tuned whitespace;

more antiquotations -- avoid unchecked string literals;

distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
some notes about missing ML interface;

tuned white space;
avoid "object-oriented English";

proper Isabelle symbols -- no UTF8 here;

tuned headers

generate elim rules for elimination of function equalities;
added fun_cases command;
recover proper cases rules for mutual recursive case (no sum types)