Make "modern" Definition syntax extensible

[dnezam]

Currently, the attributes for the "modern" Definition syntax seem to be fixed. This means that in some cases one has to fall back on using the "old" style Define. For example,

val _ = PmatchHeuristics.with_classic_heuristic Define `foo = ...`;

could be more nicely written if one could register PmatchHeuristics.with_classic_heuristic as an attribute, resulting in something like

Definition foo_def[with_classic_heuristic]:
  foo = ...
End

(courtesy of @mn200 on Discord)