proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
proper context for assume_tac (atac remains as fall-back without context);
more antiquotations;
removed old CVS Ids; tuned headers;
removed obsolete ML files;
slight adaptions to library changes
expanded tabs
Initial revision