removed a few global names in Nitpick (styp, nat_less, pairf)

add_expand_thm: explicit indication of is_def instead of fragile heuristic, tuned signature; explicit extraction_expand vs. extraction_expand_def attribute;

axiomatization: declare Spec_Rules, direct result;

use simultaneous Morphics.fact;

primitive defs: clarified def (axiom name) vs. description;

eliminated obsolete thm position tags;

permissive AList.merge -- most likely setup for theory data (beware of spurious AList.DUP);

provide actual Nitpick_HOL.extended_context;

tuned;

more accurate dependencies;