moved remaining display.ML to more_thm.ML;

prefer tactics with explicit context;

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);

proper context for match_tac etc.;

modernized functor names;
tuned;

eliminated Display.string_of_thm_without_context;
tuned whitespace;

tuned titles

removed old CVS Ids;
tuned headers;

proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

structure Display: less pervasive operations;

slight adaptions to library changes

Move towards standard functions.

renamed rep_claset to rep_cs

adapted to new sort function;

expanded tabs

chain_tac: deleted; just use etac mp

Initial revision