merge : tag -> tag -> tag
STRUCTURE
SYNOPSIS
Combine two tags into one.
DESCRIPTION
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.
SEEALSO
HOL  Kananaskis-13