tag
Thm.tag : thm -> tag
Extract the tag from a theorem.
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 = [oracles: #] [axioms: ]: tag
> Thm.tag NOT_FORALL_THM;
val it = [oracles: #] [axioms: ]: tag