1\DOC merge
2
3\TYPE {merge : tag -> tag -> tag}
4
5\SYNOPSIS
6Combine two tags into one.
7
8\KEYWORDS
9tag, oracle, inference.
10
11\DESCRIBE
12When two theorems interact via inference, their tags are merged. This
13propagates to the new theorem the fact that either or both were
14constructed via shortcut.
15
16\FAILURE
17Never fails.
18
19\EXAMPLE
20{
21- Tag.merge (Tag.read "foo") (Tag.read "bar");
22> val it = Kerneltypes.TAG(["bar", "foo"], []) : tag
23
24- Tag.merge it (Tag.read "foo");
25> val it = Kerneltypes.TAG(["bar", "foo"], []) : tag
26}
27
28
29\COMMENTS
30Although it is not harmful to use this entrypoint, there is little reason
31to, since the merge operation is only used inside the HOL kernel.
32
33\SEEALSO
34Tag.read, Thm.mk_oracle_thm, Thm.tag.
35\ENDDOC
36