Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

isEmpty

Tag.isEmpty : tag -> bool

Tells if a tag is empty.

An invocation isEmpty t returns true just in case t is the empty tag. Only theorems built solely by HOL proof have an empty tag.

Failure

Never fails.

Example

> Tag.isEmpty (Thm.tag NOT_FORALL_THM);
val it = false: bool

See also

Thm.tag, Thm.mk_oracle_thm