----------------------------------------------------------------------
thm                                                              (Thm)
----------------------------------------------------------------------
type thm

SYNOPSIS
Type of theorems of the HOL logic.

KEYWORDS
theorem, primitive inference.

DESCRIBE
The abstract type {thm} represents the theorems derivable by inference
in the HOL logic. The type of theorems can be viewed as the inductive closure
of the axioms of the HOL logic by the primitive inference rules of HOL.
Robin Milner had the brilliant insight to implement this view by encapsulating
the primitive rules of inference for a logic as the constructors for
an abstract type of theorems. This implementation technique is adopted in HOL.

SEEALSO
Thm.dest_thm, Thm.hyp, Thm.concl, Thm.tag, Thm.ASSUME, Thm.REFL,
Thm.BETA_CONV, Thm.ABS, Thm.DISCH, Thm.MP, Thm.SUBST, Thm.INST_TYPE.

----------------------------------------------------------------------