isEmpty : tag -> bool
STRUCTURE
Tag
SYNOPSIS
Tells if a tag is empty.
DESCRIPTION
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 = true : bool
SEEALSO
tag
,
mk_oracle_thm
HOL
Kananaskis-14