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