add_tag : tag * thm -> thm
STRUCTURE
SYNOPSIS
Adds oracle tags to a theorem.
DESCRIPTION
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.
SEEALSO
HOL  Trindemossen-1