A call to add_tag(tg,th) returns a th' such that calling
Thm.tag(th') returns the tag that is the merge of the tag associated
with th (if any) and tg.
FAILURE
Never fails.
COMMENTS
If an oracle implementation wishes to record additional information
about the oracle mechanisms that have contributed to the ‘proof’ of a
theorem (perhaps the use of existing HOL theorems that will have their
own tags), then this function can be used to add that record.