1\DOC isEmpty
2
3\TYPE {isEmpty : tag -> bool}
4
5\SYNOPSIS
6Tells if a tag is empty.
7
8\KEYWORDS
9tag.
10
11\DESCRIBE
12An invocation {isEmpty t} returns {true} just in case {t} is the empty tag.
13Only theorems built solely by HOL proof have an empty tag.
14
15\FAILURE
16Never fails.
17
18\EXAMPLE
19{
20- Tag.isEmpty (Thm.tag NOT_FORALL_THM);
21> val it = true : bool
22}
23
24
25\SEEALSO
26Thm.tag, Thm.mk_oracle_thm.
27\ENDDOC
28