When two theorems interact via inference, their tags are merged. This
propagates to the new theorem the fact that either or both were
constructed via shortcut.
FAILURE
Never fails.
EXAMPLE
- Tag.merge (Tag.read "foo") (Tag.read "bar");
> val it = Kerneltypes.TAG(["bar", "foo"], []) : tag
- Tag.merge it (Tag.read "foo");
> val it = Kerneltypes.TAG(["bar", "foo"], []) : tag
COMMENTS
Although it is not harmful to use this entrypoint, there is little reason
to, since the merge operation is only used inside the HOL kernel.