Allow 'is alias of' entries in docfiles.

[mn200]

We have multiples across different structures (bossLib and simpLib) with the same name, and alternative spelling versions of others (e.g., strip_tac and STRIP_TAC).

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[mn200]

One issue with this is that you don't want to have to maintain multiple “alias of” pieces of information, but you do perhaps want to the information appearing in two places (e.g. lcsymtacs.qcase_tac is an alias for Q.FIND_CASE_TAC, so you might want to have the REFERENCE have a pointer from qcase_tac to FIND_CASE_TAC as well as something in the other direction).