merge
Tag.merge : tag -> tag -> tag
Combine two tags into one.
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 = [oracles: ##] [axioms: ]: tag
> Tag.merge it (Tag.read "foo");
val it = [oracles: ##] [axioms: ]: 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.