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