renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;

document depth arguments of method "auto";

clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b); uniform handling of exceptions in depth_tac and blast_tac, discontinued separate blast_depth_tac; tuned blast_tac: atomize prems only once, outside DEEPEN;

clarified special incr_type_indexes;

tuned signature: Name.invent and Name.invent_names;

modernized structure ProofContext;

even more robust \isaspacing;

simplified Name.variant -- discontinued builtin fold_map;

some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);

discontinued Name.variant to emphasize that this is old-style / indirect;