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