Change API of Q's MATCH...RENAME_TACs.

Now rather than a string list hanging off the end specifying which
variable bindings aren't supposed to induce a renaming, just put
underscores into the pattern in those positions.

Documentation and release notes updated.

Two new tactics in Q for renaming parts of a goal by pattern matching.

MATCH_RENAME_TAC works on the goal statement; MATCH_ASSUM_RENAME_TAC on the
assumption list. Both tactics attempt to match a pattern against the goal (or
an assumption). Matching parts of the goal are then replaced by the
corresponding pattern variables.

Useful for renaming ugly generated variable names with minimal effort. The
pattern does double duty in the assumption case: it both picks out the matching
assumption and also specifies what the new variable names should be.