prefer qualified names;

tuned;

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

eliminated aliases;

more robust exception pattern General.Subscript;

eliminated old List.nth;
tuned;

modernized structure Proof_Context;

more antiquotations;

tuned titles

map_range (and map_index) combinator

replaced String.concat by implode;
replaced String.concatWith by space_implode;
replaced (Seq.flat o Seq.map) by Seq.maps;
replaced List.mapPartial by map_filter;
replaced List.concat by flat;
replaced (flat o map) by maps, which produces less garbage;

explicit indication of Unsynchronized.ref;

trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;

qualified Subgoal.FOCUS;

trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);

replaced old METAHYPS by FOCUS;
eliminated homegrown SUBGOAL combinator -- beware of exception Subscript in body;
modernized functor names;
minimal tuning of sources;
reactivated dead quasi.ML (ever used?);

qualified Term.rename_wrt_term;

removed obsolete sign_of/sign_of_thm;

got rid of type Sign.sg;

Move towards standard functions.

Deleted Library.option type.

New transitivity reasoners for transitivity only and quasi orders.