tuned syntax -- more symbols;

isabelle update_cartouches;

more symbols;

simplifie sessions;

more Isar proof methods;

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

modernized header uniformly as section;

removed old CVS Ids;
tuned headers;

proper context for tactics derived from res_inst_tac;

removed obsolete ML files;