tag : thm -> tag
STRUCTURE
SYNOPSIS
Extract the tag from a theorem.
DESCRIPTION
An invocation tag th, where th has type thm, returns the tag of the theorem. If derivation of the theorem has appealed at some point to an oracle, the tag of that oracle will be embedded in the result. Otherwise, an empty tag is returned.
FAILURE
Never fails.
EXAMPLE
- Thm.tag (mk_thm([],F));
> val it = Kerneltypes.TAG(["MK_THM"], []) : tag

- Thm.tag NOT_FORALL_THM;
> val it = Kerneltypes.TAG([], []) : tag

SEEALSO
HOL  Trindemossen-1