fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day

compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time

merged

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;